Commit 8a5c99e5 authored by Benoit Barbot's avatar Benoit Barbot

merge

parents 1ecdafdd 5e42be9b
Pipeline #1044 failed with stages
in 4 minutes and 18 seconds
......@@ -40,7 +40,7 @@ CosmosLinux:
- mkdir build
- cd build
# - ../configure --prefix=`pwd`/../ --enable-silent-rules CXXFLAGS='-g -O0 --coverage'
- ../configure --prefix=`pwd`/../ --enable-silent-rules CXXFLAGS='-O3'
- ../configure --prefix=`pwd`/../ --enable-silent-rules CXXFLAGS='-O3 -static'
- make -j 4
- make install
- make dist
......
......@@ -9,7 +9,6 @@ find_package(GIT)
find_package(Boost 1.55)
if(Boost_FOUND)
include_directories(${Boost_INCLUDE_DIRS})
endif()
set (CMAKE_CXX_STANDARD 11)
......@@ -33,54 +32,64 @@ add_library(grml src/libgrml/expatmodelparser.cc
src/libgrml/modelwriter.cc)
add_custom_command(OUTPUT ${CMAKE_CURRENT_SOURCE_DIR}/src/ModelGenerator/Eval/Eval-parser.cc ${CMAKE_CURRENT_SOURCE_DIR}/src/ModelGenerator/Eval/Eval-scanner.cc
COMMAND ${FLEX_EXECUTABLE} -o Eval-scanner.cc --prefix=eval Eval-scanner.ll
COMMAND ${BISON_EXECUTABLE} -o Eval-parser.cc -y -p eval Eval-parser.yy
WORKING_DIRECTORY "${CMAKE_CURRENT_SOURCE_DIR}/src/ModelGenerator/Eval")
add_custom_command( OUTPUT ${CMAKE_CURRENT_SOURCE_DIR}/src/ModelGenerator/GspnParser/Gspn-scanner.cc ${CMAKE_CURRENT_SOURCE_DIR}/src/ModelGenerator/GspnParser/Gspn-parser.cc
COMMAND ${FLEX_EXECUTABLE} -o Gspn-scanner.cc --prefix=gspn Gspn-scanner.ll
COMMAND ${BISON_EXECUTABLE} -o Gspn-parser.cc -y -p gspn Gspn-parser.yy
WORKING_DIRECTORY "${CMAKE_CURRENT_SOURCE_DIR}/src/ModelGenerator/GspnParser")
add_custom_command(OUTPUT ${CMAKE_CURRENT_SOURCE_DIR}/src/ModelGenerator/LhaParser/Lha-scanner.cc ${CMAKE_CURRENT_SOURCE_DIR}/src/ModelGenerator/LhaParser/Lha-parser.cc
COMMAND ${FLEX_EXECUTABLE} -o Lha-scanner.cc --prefix=lha Lha-scanner.ll
COMMAND ${BISON_EXECUTABLE} -o Lha-parser.cc -y -p lha Lha-parser.yy
WORKING_DIRECTORY "${CMAKE_CURRENT_SOURCE_DIR}/src/ModelGenerator/LhaParser")
file(GLOB_RECURSE Cosmos_SOURCES "src/ModelGenerator/*.cpp" "src/ModelGenerator/*.cc" "src/libgrml/*.cc" "src/Simulator/BatchR.cpp" )
SET_SOURCE_FILES_PROPERTIES("src/ModelGenerator/GspnParser/Gspn-Reader.cpp" PROPERTIES OBJECT_DEPENDS ${CMAKE_CURRENT_SOURCE_DIR}/src/ModelGenerator/GspnParser/Gspn-parser.cc)
SET_SOURCE_FILES_PROPERTIES("src/ModelGenerator/Eval/Eval.cpp" PROPERTIES OBJECT_DEPENDS ${CMAKE_CURRENT_SOURCE_DIR}/src/ModelGenerator/Eval/Eval-parser.cc)
SET_SOURCE_FILES_PROPERTIES("src/ModelGenerator/LhaParser/Lha-Reader.cpp" PROPERTIES OBJECT_DEPENDS ${CMAKE_CURRENT_SOURCE_DIR}/src/ModelGenerator/LhaParser/Lha-parser.cc)
file(MAKE_DIRECTORY "${CMAKE_CURRENT_BINARY_DIR}/src/ModelGenerator/Eval/")
BISON_TARGET(EvalParser src/ModelGenerator/Eval/Eval-parser.yy
${CMAKE_CURRENT_BINARY_DIR}/src/ModelGenerator/Eval/Eval-parser.cc COMPILE_FLAGS -peval)
FLEX_TARGET(EvalScanner src/ModelGenerator/Eval/Eval-scanner.ll
${CMAKE_CURRENT_BINARY_DIR}/src/ModelGenerator/Eval/Eval-scanner.cc COMPILE_FLAGS --prefix=eval)
ADD_FLEX_BISON_DEPENDENCY(EvalScanner EvalParser)
add_library(libeval
${BISON_EvalParser_OUTPUTS}
${FLEX_EvalScanner_OUTPUTS}
src/ModelGenerator/Eval/Eval.cpp)
target_include_directories(libeval PRIVATE "src/ModelGenerator/Eval")
target_include_directories(libeval PUBLIC ${CMAKE_CURRENT_BINARY_DIR}/src/ModelGenerator/Eval)
file(MAKE_DIRECTORY "${CMAKE_CURRENT_BINARY_DIR}/src/ModelGenerator/GspnParser/")
BISON_TARGET(GrmlParser src/ModelGenerator/GspnParser/Gspn-parser.yy
${CMAKE_CURRENT_BINARY_DIR}/src/ModelGenerator/GspnParser/Gspn-parser.cc COMPILE_FLAGS -pgspn)
FLEX_TARGET(GrmlScanner src/ModelGenerator/GspnParser/Gspn-scanner.ll
${CMAKE_CURRENT_BINARY_DIR}/src/ModelGenerator/GspnParser/Gspn-scanner.cc COMPILE_FLAGS --prefix=gspn)
ADD_FLEX_BISON_DEPENDENCY(GrmlScanner GrmlParser)
add_library(libgspn
${BISON_GrmlParser_OUTPUTS}
${FLEX_GrmlScanner_OUTPUTS}
src/ModelGenerator/GspnParser/Gspn-Grml-Output.cpp
src/ModelGenerator/GspnParser/Gspn-Writer-Color.cpp
src/ModelGenerator/GspnParser/Gspn-model.cpp
src/ModelGenerator/GspnParser/unfolder.cpp
src/ModelGenerator/GspnParser/Gspn-Reader.cpp
src/ModelGenerator/GspnParser/Gspn-Writer.cpp
src/ModelGenerator/GspnParser/Gspn_gmlparser.cpp
)
target_link_libraries (libgspn grml libeval)
target_include_directories(libgspn PUBLIC "src/libgrml")
target_include_directories(libgspn PRIVATE "src/ModelGenerator/GspnParser")
target_include_directories(libgspn PUBLIC ${CMAKE_CURRENT_BINARY_DIR}/src/ModelGenerator/GspnParser)
file(MAKE_DIRECTORY "${CMAKE_CURRENT_BINARY_DIR}/src/ModelGenerator/LhaParser/")
BISON_TARGET(LHAParser src/ModelGenerator/LhaParser/Lha-parser.yy
${CMAKE_CURRENT_BINARY_DIR}/src/ModelGenerator/LhaParser/Lha-parser.cc COMPILE_FLAGS -plha)
FLEX_TARGET(LHAScanner src/ModelGenerator/LhaParser/Lha-scanner.ll
${CMAKE_CURRENT_BINARY_DIR}/src/ModelGenerator/LhaParser/Lha-scanner.cc COMPILE_FLAGS --prefix=lha)
ADD_FLEX_BISON_DEPENDENCY(LHAScanner LHAParser)
add_library(liblha
${BISON_LHAParser_OUTPUTS}
${FLEX_LHAScanner_OUTPUTS}
src/ModelGenerator/LhaParser/Lha-Reader.cpp
src/ModelGenerator/LhaParser/Lha_gmlparser.cpp
)
target_include_directories(liblha PRIVATE "src/ModelGenerator/LhaParser")
target_include_directories(liblha PRIVATE ${CMAKE_CURRENT_BINARY_DIR}/src/ModelGenerator/LhaParser)
target_link_libraries(liblha libeval libgspn)
include_directories ("src/libgrml" ${EXPAT_INCLUDE_DIR} "src/ModelGenerator" ${Boost_INCLUDE_DIR})
add_executable(Cosmos
src/Simulator/BatchR.cpp
src/ModelGenerator/Eval/Eval-parser.cc
src/ModelGenerator/GspnParser/Gspn-parser.cc
src/ModelGenerator/LhaParser/Lha-parser.cc
src/ModelGenerator/Eval/Eval-scanner.cc
src/ModelGenerator/GspnParser/Gspn-scanner.cc
src/ModelGenerator/LhaParser/Lha-scanner.cc
src/ModelGenerator/Eval/Eval.cpp
src/ModelGenerator/GspnParser/Gspn-Grml-Output.cpp
src/ModelGenerator/GspnParser/Gspn-Writer-Color.cpp
src/ModelGenerator/GspnParser/Gspn-model.cpp
src/ModelGenerator/GspnParser/unfolder.cpp
src/ModelGenerator/GspnParser/Gspn-Reader.cpp
src/ModelGenerator/GspnParser/Gspn-Writer.cpp
src/ModelGenerator/GspnParser/Gspn_gmlparser.cpp
src/ModelGenerator/LhaParser/Lha-Reader.cpp
src/ModelGenerator/LhaParser/Lha_gmlparser.cpp
src/ModelGenerator/Cosmos.cpp
src/ModelGenerator/HaslFormula.cpp
src/ModelGenerator/expressionStruct.cpp
src/ModelGenerator/expressionStruct.cpp
src/ModelGenerator/result.cpp
src/ModelGenerator/Generator.cpp
src/ModelGenerator/casesWriter.cpp
......@@ -88,11 +97,13 @@ add_executable(Cosmos
src/ModelGenerator/SimpleSerializer.cpp
src/ModelGenerator/server.cpp)
target_link_libraries (Cosmos grml ${EXPAT_LIBRARY} ${Boost_LIBRARIES})
target_include_directories(Cosmos PRIVATE "src/ModelGenerator/GspnParser")
target_include_directories(Cosmos PRIVATE "src/ModelGenerator/LhaParser")
target_include_directories(Cosmos PRIVATE "${CMAKE_CURRENT_BINARY_DIR}/src/ModelGenerator/LhaParser")
target_link_libraries (Cosmos grml liblha ${EXPAT_LIBRARY})
install(TARGETS Cosmos DESTINATION bin)
add_library(ClientSimBase
src/ModelGenerator/parameters.cpp
src/ModelGenerator/SimpleSerializer.cpp
......@@ -104,11 +115,14 @@ add_library(ClientSimBase
src/Simulator/clientsim.cpp
src/Simulator/Simulator.cpp
)
target_include_directories(ClientSimBase PRIVATE "src/ModelGenerator")
install(TARGETS ClientSimBase DESTINATION lib)
add_library(ClientSimMain
src/Simulator/timeGenBis.cpp
src/Simulator/main.cpp
)
target_include_directories(ClientSimMain PRIVATE "src/ModelGenerator")
install(TARGETS ClientSimMain DESTINATION lib)
add_library(ClientSim
......@@ -127,6 +141,7 @@ add_library(ClientSim
src/Simulator/Simulink/SKTime.cpp
src/Simulator/InstanceSPNSim.cpp
)
target_include_directories(ClientSim PRIVATE "src/ModelGenerator")
install(TARGETS ClientSim DESTINATION lib)
......@@ -174,7 +189,7 @@ SOURCES ${ml_SOURCES}
add_executable(testClientSim ${CMAKE_CURRENT_BINARY_DIR}/tmp/spn.cpp ${CMAKE_CURRENT_BINARY_DIR}/tmp/LHA.cpp)
include_directories("src/Simulator")
add_dependencies(testClientSim Cosmos)
target_link_libraries (testClientSim ClientSimMain ClientSimBase ${Boost_LIBRARIES})
target_link_libraries (testClientSim ClientSimMain ClientSimBase)
enable_testing()
......
This source diff could not be displayed because it is too large. You can view the blob instead.
This diff is collapsed.
This diff is collapsed.
Cosmos 802.11pOneMedium.grml simpleprop2.cpp --tmp-status 2 --batch 0 --max-run 100 --const "Arrival=$1" --njob=2 --HASL-formula "Throughput_CorrectPacketAckp1= AVG(Last(Garbled));
Throughput_CorrectPacketAckp2= AVG(Last(Garbled));
Throughput_CorrectPacketAckp3= AVG(Last(Garbled));
Throughput_CorrectPacketAckp4= AVG(Last(Garbled));
Throughput_CorrectPacketAck12= AVG(Last(Garbled));
Throughput_CorrectPacketAck21= AVG(Last(Garbled));
MeanToken_Idle= AVG(Last( Idle));
MeanToken_Medium= AVG(Last( Medium));
MeanToken_Garbled= AVG(Last( Garbled));" > res_$1.res
\ No newline at end of file
#include <iostream>
#include <algorithm>
#include <vector>
using namespace std;
#include "markingImpl.hpp"
#include <math.h>
#include <float.h>
#include "LHA.hpp"
const double AIFS1=2;
const double AIFS2=3;
const double AIFS3=6;
const double AIFS4=9;
const double Ack=11;
const double Arrival=0.001;
const double CTS=11;
const double Data=200;
const double N=2;
const double RTS=16;
const double SIFS=1;
const double T=10000;
const double Timeout=5;
const double Traffic=1;
const double Ttrans=0;
const double Vuln=2;
const double aSlot=1;
const double f=2;
const double invT=0.0001;
namespace hybridVar {
};
struct Variables {
double time;
double countT;
double CorrectPacketAckp1;
double CorrectPacketAckp2;
double CorrectPacketAckp3;
double CorrectPacketAckp4;
double PLVAR_Idle;
double PLVAR_Medium;
double PLVAR_Garbled;
double CorrectPacketAck12;
double CorrectPacketAck21;
};
bool varOrder(const Variables &v1,const Variables &v2){
if(v1.time<v2.time)return true;
if(v1.countT<v2.countT)return true;
if(v1.CorrectPacketAckp1<v2.CorrectPacketAckp1)return true;
if(v1.CorrectPacketAckp2<v2.CorrectPacketAckp2)return true;
if(v1.CorrectPacketAckp3<v2.CorrectPacketAckp3)return true;
if(v1.CorrectPacketAckp4<v2.CorrectPacketAckp4)return true;
if(v1.PLVAR_Idle<v2.PLVAR_Idle)return true;
if(v1.PLVAR_Medium<v2.PLVAR_Medium)return true;
if(v1.PLVAR_Garbled<v2.PLVAR_Garbled)return true;
if(v1.CorrectPacketAck12<v2.CorrectPacketAck12)return true;
if(v1.CorrectPacketAck21<v2.CorrectPacketAck21)return true;
return false;
};
template<class DEDState>
void LHA<DEDState>::resetVariables(){
Vars->time= 0;
Vars->countT= 0;
Vars->CorrectPacketAckp1= 0;
Vars->CorrectPacketAckp2= 0;
Vars->CorrectPacketAckp3= 0;
Vars->CorrectPacketAckp4= 0;
Vars->PLVAR_Idle= 0;
Vars->PLVAR_Medium= 0;
Vars->PLVAR_Garbled= 0;
Vars->CorrectPacketAck12= 0;
Vars->CorrectPacketAck21= 0;
};
template<class DEDState>
void LHA<DEDState>::printHeader(ostream &s)const{
s << " Location\t";
};
template<class DEDState>
void LHA<DEDState>::printState(ostream &s){
s << "\t" << LocLabel[CurrentLocation] << "\t";
};
template<class DEDState>
const int LHA<DEDState>::ActionEdgesAr[] = {
1 ,1 ,1 ,1 ,1 ,1 ,1 ,1 ,1 ,1 ,1 ,1 ,1 ,1 ,1 ,1 ,1 ,1 ,1 ,1 ,1 ,1 ,1 ,1 ,1 ,1 ,1 ,1 ,1 ,1 ,1 ,1 ,1 ,1 ,1 ,1 ,1 ,1 ,1 ,1 ,1 ,1 ,1 ,1 ,1 ,1 ,1 ,1 ,1 ,1 ,1 ,1 ,1 ,1 ,1 ,1 ,1 ,1 ,1 ,1 ,4 ,1 ,1 ,1 ,1 ,1 ,1 ,1 ,1 ,1 ,1 ,1 ,1 ,1 ,1 ,1 ,1 ,1 ,0 ,0 ,0 ,0 ,0 ,0 ,0 ,0 ,0 ,0 ,0 ,0 ,0 ,0 ,0 ,0 ,0 ,0 ,0 ,0 ,0 ,0 ,0 ,0 ,0 ,0 ,0 ,0 ,0 ,0 ,0 ,0 ,0 ,0 ,0 ,0 ,0 ,0 ,0 ,
0 ,0 ,0 ,0 ,0 ,0 ,0 ,0 ,0 ,0 ,0 ,0 ,0 ,0 ,0 ,0 ,0 ,0 ,0 ,0 ,0 ,0 ,0 ,0 ,0 ,0 ,0 ,0 ,0 ,0 ,0 ,0 ,0 ,0 ,0 ,0 ,0 ,0 ,0 ,6 ,6 ,6 ,6 ,6 ,6 ,6 ,6 ,6 ,6 ,6 ,6 ,6 ,6 ,6 ,6 ,6 ,6 ,6 ,6 ,6 ,2 ,6 ,6 ,6 ,6 ,6 ,6 ,6 ,6 ,6 ,6 ,6 ,6 ,6 ,6 ,6 ,6 ,6 ,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,
-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,3 ,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,
-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,4 ,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,
-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,5 ,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,};
template<class DEDState>
LHA<DEDState>::LHA():NbLoc(3),NbTrans(39),NbVar(11),FinalLoc( 3,false){
InitLoc.insert(0);
FinalLoc[2]=true;
Edge= vector<LhaEdge>(8);
Edge[0] = LhaEdge(0, 0, 0,Synch);
Edge[1] = LhaEdge(1, 0, 1,Auto);
Edge[2] = LhaEdge(2, 1, 1,Synch);
Edge[3] = LhaEdge(3, 1, 1,Synch);
Edge[4] = LhaEdge(4, 1, 1,Synch);
Edge[5] = LhaEdge(5, 1, 1,Synch);
Edge[6] = LhaEdge(6, 1, 1,Synch);
Edge[7] = LhaEdge(7, 1, 2,Auto);
Vars = new Variables;
tempVars = new Variables;
resetVariables();
Out_A_Edges =vector< set < int > >(NbLoc);
Out_A_Edges[0].insert(1);
Out_A_Edges[1].insert(7);
LinForm= vector<double>(9,0.0);
OldLinForm=vector<double>(9,0.0);
LhaFunc=vector<double>(9,0.0);
LhaFuncDefaults=vector<double>(9,0.0);
FormulaVal = vector<double>(9,0.0);
FormulaValQual = vector<bool>(0,false);
}
template<class DEDState>
void LHA<DEDState>::DoElapsedTimeUpdate(double DeltaT,const DEDState& Marking) {
Vars->time += GetFlow(0, Marking) * DeltaT;
Vars->CorrectPacketAckp1 += GetFlow(2, Marking) * DeltaT;
Vars->CorrectPacketAckp2 += GetFlow(3, Marking) * DeltaT;
Vars->CorrectPacketAckp3 += GetFlow(4, Marking) * DeltaT;
Vars->CorrectPacketAckp4 += GetFlow(5, Marking) * DeltaT;
Vars->PLVAR_Idle += GetFlow(6, Marking) * DeltaT;
Vars->PLVAR_Medium += GetFlow(7, Marking) * DeltaT;
Vars->PLVAR_Garbled += GetFlow(8, Marking) * DeltaT;
Vars->CorrectPacketAck12 += GetFlow(9, Marking) * DeltaT;
Vars->CorrectPacketAck21 += GetFlow(10, Marking) * DeltaT;
}
template<class DEDState>
double LHA<DEDState>::GetFlow(int v, const DEDState& Marking)const{
switch (v){
case 1: //countT
break;
case 8: //PLVAR_Garbled
switch (CurrentLocation){
case 1: //l1
return Marking.P->_PL_Garbled * 0.0001;
break;
default: //l0,l2,
return 0.0;
break;
}
break;
case 6: //PLVAR_Idle
switch (CurrentLocation){
case 1: //l1
return Marking.P->_PL_Idle.card() * 0.0001;
break;
default: //l0,l2,
return 0.0;
break;
}
break;
case 7: //PLVAR_Medium
switch (CurrentLocation){
case 1: //l1
return Marking.P->_PL_Medium * 0.0001;
break;
default: //l0,l2,
return 0.0;
break;
}
break;
case 0: //time
switch (CurrentLocation){
case 2: //l2
return 0.0;
break;
default: //l0,l1,
return 1;
break;
}
break;
default: //CorrectPacketAckp1,CorrectPacketAckp2,CorrectPacketAckp3,CorrectPacketAckp4,CorrectPacketAck12,CorrectPacketAck21,
return 0.0;
break;
}
}
template<class DEDState>
bool LHA<DEDState>::CheckLocation(int loc,const DEDState& Marking)const{
return true;
}
template<class DEDState>
bool LHA<DEDState>::CheckEdgeContraints(int ed,size_t ptt,const abstractBinding& b,const DEDState& Marking)const{
switch (ed){
case 0: //
{
if(!( +(1)*Vars->time<=0)) return false;
return (true);
}
break;
case 6: //
{
if(!( +(1)*Vars->time<=10000)) return false;
return (true);
}
break;
case 2: //
{
if( b.P->p.c0 != Color_Pr_pr1 )return false;
if(!( +(1)*Vars->time<=10000)) return false;
return (true);
}
break;
case 3: //
{
if( b.P->p.c0 != Color_Pr_pr2 )return false;
if(!( +(1)*Vars->time<=10000)) return false;
return (true);
}
break;
case 4: //
{
if( b.P->p.c0 != Color_Pr_pr3 )return false;
if(!( +(1)*Vars->time<=10000)) return false;
return (true);
}
break;
case 5: //
{
if( b.P->p.c0 != Color_Pr_pr4 )return false;
if(!( +(1)*Vars->time<=10000)) return false;
return (true);
}
break;
default: //,,
return true;
break;
}
}
template<class DEDState>
t_interval LHA<DEDState>::GetEdgeEnablingTime(int ed,const DEDState& Marking)const{
switch (ed){
case 1: //
{
t_interval EnablingT;
EnablingT.first=CurrentTime;
EnablingT.second=DBL_MAX;
t_interval EmptyInterval;
EmptyInterval.first=0;
EmptyInterval.second=-1;
double SumAF;
double SumAX;
SumAF=+(1)*GetFlow(0, Marking);
SumAX=+(1)*Vars->time;
if(SumAF==0){
if(!(SumAX==0))
return EmptyInterval;
}
else{
double t=CurrentTime+(0-SumAX)/(double)SumAF;
if(t>=EnablingT.first && t<=EnablingT.second){
EnablingT.first=t; EnablingT.second=t;
}
else return EmptyInterval;
}
return EnablingT;
}
break;
case 7: //
{
t_interval EnablingT;
EnablingT.first=CurrentTime;
EnablingT.second=DBL_MAX;
t_interval EmptyInterval;
EmptyInterval.first=0;
EmptyInterval.second=-1;
double SumAF;
double SumAX;
SumAF=+(1)*GetFlow(0, Marking);
SumAX=+(1)*Vars->time;
if(SumAF==0){
if(!(SumAX==10000))
return EmptyInterval;
}
else{
double t=CurrentTime+(10000-SumAX)/(double)SumAF;
if(t>=EnablingT.first && t<=EnablingT.second){
EnablingT.first=t; EnablingT.second=t;
}
else return EmptyInterval;
}
return EnablingT;
}
break;
default: //,,,,,,
{
t_interval EnablingT;
EnablingT.first=CurrentTime;
EnablingT.second=DBL_MAX;
return EnablingT;
}
break;
}
}
template<class DEDState>
void LHA<DEDState>::DoEdgeUpdates(int ed,const DEDState& Marking, const abstractBinding& b){
switch (ed){
case 6: //
{
Vars->countT=Vars->countT + 1;
}
break;
case 1: //
{
Vars->time=0;
}
break;
case 2: //
{
tempVars->countT=Vars->countT + 1;
tempVars->CorrectPacketAckp1=Vars->CorrectPacketAckp1 + 1;
if(b.P->sa.c0 == Color_St_s1){Vars->CorrectPacketAck12+= 1;}else{Vars->CorrectPacketAck21+= 1;}
Vars->countT = tempVars->countT;
Vars->CorrectPacketAckp1 = tempVars->CorrectPacketAckp1;
}
break;
case 3: //
{
tempVars->countT=Vars->countT + 1;
tempVars->CorrectPacketAckp2=Vars->CorrectPacketAckp2 + 1;
if(b.P->sa.c0 == Color_St_s1){Vars->CorrectPacketAck12+= 1;}else{Vars->CorrectPacketAck21+= 1;}
Vars->countT = tempVars->countT;
Vars->CorrectPacketAckp2 = tempVars->CorrectPacketAckp2;
}
break;
case 4: //
{
tempVars->countT=Vars->countT + 1;
tempVars->CorrectPacketAckp3=Vars->CorrectPacketAckp3 + 1;
if(b.P->sa.c0 == Color_St_s1){Vars->CorrectPacketAck12+= 1;}else{Vars->CorrectPacketAck21+= 1;}
Vars->countT = tempVars->countT;
Vars->CorrectPacketAckp3 = tempVars->CorrectPacketAckp3;
}
break;
case 5: //
{
tempVars->countT=Vars->countT + 1;
tempVars->CorrectPacketAckp4=Vars->CorrectPacketAckp4 + 1;
if(b.P->sa.c0 == Color_St_s1){Vars->CorrectPacketAck12+= 1;}else{