progress

Examples/Wifi802.11/802.11.PNPRO

@@ -1600,11 +1600,11 @@
       <transition delay="I[AIFS1]" name="WaitAIFS1" type="GEN" x="101.55" y="26.0"/>
       <place domain="P" label-x="0.5" label-y="-2.0" name="Vulnerable" x="114.0" y="26.0"/>
       <place domain="P" name="Sending" x="129.0" y="26.0"/>
-      <place domain="P" marking="&lt;St,s1,pr1,rts&gt;" name="WaitForResponse" x="111.0" y="42.0"/>
+      <place domain="P" marking="&lt;s1,s2,pr1,rts&gt;+&lt;s2,s1,pr1,rts&gt;" name="WaitForResponse" x="111.0" y="42.0"/>
       <place domain="P" name="Receiving" x="101.0" y="42.0"/>
       <place name="Medium" x="121.0" y="12.0"/>
-      <transition delay="I[Vuln]" name="BeginSending" type="GEN" x="122.55" y="26.0"/>
-      <place domain="P" name="SentPacket" x="135.0" y="12.0"/>
+      <transition delay="I[Vuln]" label-y="-2.0" name="BeginSending" type="GEN" x="122.55" y="26.0"/>
+      <place domain="P" name="SentPacket" x="136.0" y="15.0"/>
       <transition name="PacketLoss" rotation="1.5707963267948966" type="IMM" x="135.85" y="8.0"/>
       <transition delay="I[RTS]" name="SendRTS" rotation="1.5707963267948966" type="GEN" x="119.55" y="34.0"/>
       <transition delay="I[CTS]" name="SendCTS" rotation="1.5707963267948966" type="GEN" x="125.55" y="34.0"/>
@@ -1621,7 +1621,7 @@
       <place domain="P" name="PacketSent" x="129.0" y="42.0"/>
       <transition name="BeginWaitingForResponse" type="IMM" x="122.85" y="42.0"/>
       <place domain="P" name="ReadingPacket" x="91.0" y="42.0"/>
-      <transition name="StopReceiving" priority="2" type="IMM" x="96.85" y="42.0"/>
+      <transition name="StopReceiving" type="IMM" x="96.85" y="42.0"/>
       <transition guard="pt==rts||pt==data" name="ReceiverGarbled" type="IMM" x="97.85" y="37.0"/>
       <transition delay="I[Timeout]" name="ReceiverTimeout" type="GEN" x="107.55" y="37.0"/>
       <transition guard="pt==rts||pt==data" name="ReceiverWrongPacket" type="IMM" x="88.85" y="37.0"/>
@@ -1670,6 +1670,7 @@
       <transition delay="I[AIFS3]" name="ResumeBackoff3" type="GEN" x="25.55" y="43.0"/>
       <transition delay="I[AIFS4]" name="ResumeBackoff4" type="GEN" x="25.55" y="47.0"/>
       <constant consttype="REAL" name="Arrival" value="0.001" x="4.0625" y="20.0"/>
+      <place name="P0" x="139.0" y="8.0"/>
     </nodes>
     <edges>
       <arc head="PacketArrival" kind="INPUT" mult="&lt;sa,p&gt;" mult-k="0.35712890625000004" tail="Idle"/>
@@ -1692,7 +1693,7 @@
       </arc>
       <arc broken="true" head="Medium" kind="OUTPUT" mult-k="2.5729339599609373" tail="BeginSending">
         <point x="132.0" y="24.0"/>
-        <point x="116.0" y="16.0"/>
+        <point x="117.5" y="18.5"/>
       </arc>
       <arc broken="true" head="SendAck" kind="INPUT" tail="Medium">
         <point x="129.0" y="11.5"/>
@@ -1762,7 +1763,7 @@
         <point x="128.0" y="16.0"/>
         <point x="136.0" y="50.0"/>
       </arc>
-      <arc head="StopReceiving" kind="INPUT" mult="&lt;sa,sb,p,pt&gt;" mult-x="0.0" mult-y="-0.5" tail="Receiving"/>
+      <arc head="StopReceiving" kind="INPUT" mult="&lt;sa,sb,p,pt&gt;" mult-k="0.39990234375" mult-x="0.0" mult-y="-0.5" tail="Receiving"/>
       <arc head="ReadingPacket" kind="OUTPUT" mult="&lt;sa,sb,p,pt&gt;" mult-x="0.5" mult-y="-0.5" tail="StopReceiving"/>
       <arc broken="true" head="StopReceiving" kind="INHIBITOR" mult-k="2.6971466064453127" tail="Medium">
         <point x="115.5" y="19.0"/>
@@ -1821,8 +1822,8 @@
         <point x="83.5" y="36.0"/>
       </arc>
       <arc broken="true" head="CorrectPacketAck" kind="INPUT" mult="&lt;sb,sa,p,pt&gt;" mult-k="2.8349382817745212" mult-x="2.0" mult-y="0.49855245943534143" tail="SentPacket">
-        <point x="146.5" y="17.5"/>
-        <point x="68.5" y="34.5"/>
+        <point x="150.5" y="17.0"/>
+        <point x="72.5" y="34.0"/>
       </arc>
       <arc broken="true" head="Idle" kind="OUTPUT" mult="&lt;sa,p&gt;" mult-k="2.8481939584016804" mult-y="-3.1032385855134237E-4" tail="CorrectPacketAck">
         <point x="89.5" y="37.5"/>
@@ -1997,6 +1998,7 @@
       <arc broken="true" head="ResumeBackoff2" kind="INHIBITOR" mult-k="1.513446044921875" tail="Medium">
         <point x="37.0" y="39.5"/>
       </arc>
+      <arc head="PacketLoss" kind="INPUT" tail="P0"/>
     </edges>
   </gspn>
   <gspn name="802.11pTopo" zoom="150">

Examples/Wifi802.11/exp2/run.sh

+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

Examples/Wifi802.11/exp2/simpleprop2.cpp

+#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{Vars->CorrectPacketAck21+= 1;}
+             Vars->countT = tempVars->countT;
+		Vars->CorrectPacketAckp4 = tempVars->CorrectPacketAckp4;
+         }
+
+		break;
+	}
+}
+
+template<class DEDState>
+void LHA<DEDState>::UpdateLinForm(const DEDState& Marking){
+    }
+
+template<class DEDState>
+void LHA<DEDState>::UpdateLhaFunc(double& Delta ){
+
+    }
+
+template<class DEDState>
+void LHA<DEDState>::UpdateFormulaVal(const DEDState& Marking){
+
+    LhaFunc[0]= Vars->CorrectPacketAckp1;
+    LhaFunc[1]= Vars->CorrectPacketAckp2;
+    LhaFunc[2]= Vars->CorrectPacketAckp3;
+    LhaFunc[3]= Vars->CorrectPacketAckp4;
+    LhaFunc[4]= Vars->CorrectPacketAck12;
+    LhaFunc[5]= Vars->CorrectPacketAck21;
+    LhaFunc[6]= Vars->PLVAR_Idle;
+    LhaFunc[7]= Vars->PLVAR_Medium;
+    LhaFunc[8]= Vars->PLVAR_Garbled;
+    FormulaVal[0]=LhaFunc[0];
+    FormulaVal[1]=LhaFunc[1];
+    FormulaVal[2]=LhaFunc[2];
+    FormulaVal[3]=LhaFunc[3];
+    FormulaVal[4]=LhaFunc[4];
+    FormulaVal[5]=LhaFunc[5];
+    FormulaVal[6]=LhaFunc[6];
+    FormulaVal[7]=LhaFunc[7];
+    FormulaVal[8]=LhaFunc[8];
+}
+
+bool IsLHADeterministic = 1;
+fullState::fullState():loc(0){
+	var= new Variables;
+}
+
+fullState::fullState(int l,const Variables &v):loc(l){
+	var= new Variables(v);
+}
+
+fullState::fullState(const fullState &fs):loc(fs.loc){
+	var= new Variables(*(fs.var));
+}
+
+fullState::~fullState(){delete var;}
+
+template class LHA<abstractMarking>;

Examples/Wifi802.11/simpleprop.cpp

@@ -345,7 +345,7 @@ void LHA<DEDState>::DoEdgeUpdates(int ed,const DEDState& Marking, const abstract
 		case 2:	//
          {
 		tempVars->countT=Vars->countT + 1;
-		tempVars->CorrectPacketAckp1=Vars->CorrectPacketAckp1 + 0.0001;
+		tempVars->CorrectPacketAckp1=Vars->CorrectPacketAckp1 + 1;
 		Vars->countT = tempVars->countT;
 		Vars->CorrectPacketAckp1 = tempVars->CorrectPacketAckp1;
          }
@@ -354,7 +354,7 @@ void LHA<DEDState>::DoEdgeUpdates(int ed,const DEDState& Marking, const abstract
 		case 3:	//
          {
 		tempVars->countT=Vars->countT + 1;
-		tempVars->CorrectPacketAckp2=Vars->CorrectPacketAckp2 + 0.0001;
+		tempVars->CorrectPacketAckp2=Vars->CorrectPacketAckp2 + 1;
 		Vars->countT = tempVars->countT;
 		Vars->CorrectPacketAckp2 = tempVars->CorrectPacketAckp2;
          }
@@ -363,7 +363,7 @@ void LHA<DEDState>::DoEdgeUpdates(int ed,const DEDState& Marking, const abstract
 		case 4:	//
          {
 		tempVars->countT=Vars->countT + 1;
-		tempVars->CorrectPacketAckp3=Vars->CorrectPacketAckp3 + 0.0001;
+		tempVars->CorrectPacketAckp3=Vars->CorrectPacketAckp3 + 1;
 		Vars->countT = tempVars->countT;
 		Vars->CorrectPacketAckp3 = tempVars->CorrectPacketAckp3;
          }
@@ -372,7 +372,7 @@ void LHA<DEDState>::DoEdgeUpdates(int ed,const DEDState& Marking, const abstract
 		case 5:	//
          {
 		tempVars->countT=Vars->countT + 1;
-		tempVars->CorrectPacketAckp4=Vars->CorrectPacketAckp4 + 0.0001;
+		tempVars->CorrectPacketAckp4=Vars->CorrectPacketAckp4 + 1;
 		Vars->countT = tempVars->countT;
 		Vars->CorrectPacketAckp4 = tempVars->CorrectPacketAckp4;
          }

Examples/Wifi802.11/simpleprop.lha

 const double T=10000;
 const double invT=0.0001;
 const double Ttrans= 0;
-VariablesList = {time,DISC countT, CorrectPacketAckp1,CorrectPacketAckp2,CorrectPacketAckp3,CorrectPacketAckp4,PLVAR_Idle, PLVAR_Medium, PLVAR_Garbled} ;
+VariablesList = {time,DISC countT, CorrectPacketAckp1,CorrectPacketAckp2,CorrectPacketAckp3,CorrectPacketAckp4,PLVAR_Idle, PLVAR_Medium, PLVAR_Garbled, CorrectPacketAck12, CorrectPacketAck21} ;
 LocationsList = {l0, l1,l2};
 Throughput_CorrectPacketAckp1= AVG(Last(CorrectPacketAckp1));
 Throughput_CorrectPacketAckp2= AVG(Last(CorrectPacketAckp2));
 Throughput_CorrectPacketAckp3= AVG(Last(CorrectPacketAckp3));
 Throughput_CorrectPacketAckp4= AVG(Last(CorrectPacketAckp4));
+Throughput_CorrectPacketAck12= AVG(Last(CorrectPacketAck12));