diff --git a/examples/pmdp/firewire/firewire.nm b/examples/pmdp/firewire/firewire.nm new file mode 100644 index 000000000..19ecd4ed7 --- /dev/null +++ b/examples/pmdp/firewire/firewire.nm @@ -0,0 +1,176 @@ +// firewire protocol with integer semantics +// dxp/gxn 14/06/01 + +// CLOCKS +// x1 (x2) clock for node1 (node2) +// y1 and y2 (z1 and z2) clocks for wire12 (wire21) + +mdp + +// maximum and minimum delays +// fast +const int rc_fast_max = 85; +const int rc_fast_min = 76; +// slow +const int rc_slow_max = 167; +const int rc_slow_min = 159; +// delay caused by the wire length +const int delay; +// probability of choosing fast +const double fast1; // = 0.5; +const double slow1=1-fast1; +const double fast2; // = 0.5; +const double slow2=1-fast2; + +module wire12 + + // local state + w12 : [0..9]; + // 0 - empty + // 1 - rec_req + // 2 - rec_req_ack + // 3 - rec_ack + // 4 - rec_ack_idle + // 5 - rec_idle + // 6 - rec_idle_req + // 7 - rec_ack_req + // 8 - rec_req_idle + // 9 - rec_idle_ack + + // clock for wire12 + y1 : [0..delay+1]; + y2 : [0..delay+1]; + + // empty + // do not need y1 and y2 to increase as always reset when this state is left + // similarly can reset y1 and y2 when we re-enter this state + [snd_req12] w12=0 -> (w12'=1) & (y1'=0) & (y2'=0); + [snd_ack12] w12=0 -> (w12'=3) & (y1'=0) & (y2'=0); + [snd_idle12] w12=0 -> (w12'=5) & (y1'=0) & (y2'=0); + [time] w12=0 -> (w12'=w12); + // rec_req + [snd_req12] w12=1 -> (w12'=1); + [rec_req12] w12=1 -> (w12'=0) & (y1'=0) & (y2'=0); + [snd_ack12] w12=1 -> (w12'=2) & (y2'=0); + [snd_idle12] w12=1 -> (w12'=8) & (y2'=0); + [time] w12=1 & y2 (y1'=min(y1+1,delay+1)) & (y2'=min(y2+1,delay+1)); + // rec_req_ack + [snd_ack12] w12=2 -> (w12'=2); + [rec_req12] w12=2 -> (w12'=3); + [time] w12=2 & y1 (y1'=min(y1+1,delay+1)) & (y2'=min(y2+1,delay+1)); + // rec_ack + [snd_ack12] w12=3 -> (w12'=3); + [rec_ack12] w12=3 -> (w12'=0) & (y1'=0) & (y2'=0); + [snd_idle12] w12=3 -> (w12'=4) & (y2'=0); + [snd_req12] w12=3 -> (w12'=7) & (y2'=0); + [time] w12=3 & y2 (y1'=min(y1+1,delay+1)) & (y2'=min(y2+1,delay+1)); + // rec_ack_idle + [snd_idle12] w12=4 -> (w12'=4); + [rec_ack12] w12=4 -> (w12'=5); + [time] w12=4 & y1 (y1'=min(y1+1,delay+1)) & (y2'=min(y2+1,delay+1)); + // rec_idle + [snd_idle12] w12=5 -> (w12'=5); + [rec_idle12] w12=5 -> (w12'=0) & (y1'=0) & (y2'=0); + [snd_req12] w12=5 -> (w12'=6) & (y2'=0); + [snd_ack12] w12=5 -> (w12'=9) & (y2'=0); + [time] w12=5 & y2 (y1'=min(y1+1,delay+1)) & (y2'=min(y2+1,delay+1)); + // rec_idle_req + [snd_req12] w12=6 -> (w12'=6); + [rec_idle12] w12=6 -> (w12'=1); + [time] w12=6 & y1 (y1'=min(y1+1,delay+1)) & (y2'=min(y2+1,delay+1)); + // rec_ack_req + [snd_req12] w12=7 -> (w12'=7); + [rec_ack12] w12=7 -> (w12'=1); + [time] w12=7 & y1 (y1'=min(y1+1,delay+1)) & (y2'=min(y2+1,delay+1)); + // rec_req_idle + [snd_idle12] w12=8 -> (w12'=8); + [rec_req12] w12=8 -> (w12'=5); + [time] w12=8 & y1 (y1'=min(y1+1,delay+1)) & (y2'=min(y2+1,delay+1)); + // rec_idle_ack + [snd_ack12] w12=9 -> (w12'=9); + [rec_idle12] w12=9 -> (w12'=3); + [time] w12=9 & y1 (y1'=min(y1+1,delay+1)) & (y2'=min(y2+1,delay+1)); + +endmodule + +module node1 + + // clock for node1 + x1 : [0..168]; + + // local state + s1 : [0..8]; + // 0 - root contention + // 1 - rec_idle + // 2 - rec_req_fast + // 3 - rec_req_slow + // 4 - rec_idle_fast + // 5 - rec_idle_slow + // 6 - snd_req + // 7- almost_root + // 8 - almost_child + + // added resets to x1 when not considered again until after rest + // removed root and child (using almost root and almost child) + + // root contention immediate state) + [snd_idle12] s1=0 -> fast1 : (s1'=2) & (x1'=0) + slow1 : (s1'=3) & (x1'=0); + [rec_idle21] s1=0 -> (s1'=1); + // rec_idle immediate state) + [snd_idle12] s1=1 -> fast1 : (s1'=4) & (x1'=0) + slow1 : (s1'=5) & (x1'=0); + [rec_req21] s1=1 -> (s1'=0); + // rec_req_fast + [rec_idle21] s1=2 -> (s1'=4); + [snd_ack12] s1=2 & x1>=rc_fast_min -> (s1'=7) & (x1'=0); + [time] s1=2 & x1 (x1'=min(x1+1,168)); + // rec_req_slow + [rec_idle21] s1=3 -> (s1'=5); + [snd_ack12] s1=3 & x1>=rc_slow_min -> (s1'=7) & (x1'=0); + [time] s1=3 & x1 (x1'=min(x1+1,168)); + // rec_idle_fast + [rec_req21] s1=4 -> (s1'=2); + [snd_req12] s1=4 & x1>=rc_fast_min -> (s1'=6) & (x1'=0); + [time] s1=4 & x1 (x1'=min(x1+1,168)); + // rec_idle_slow + [rec_req21] s1=5 -> (s1'=3); + [snd_req12] s1=5 & x1>=rc_slow_min -> (s1'=6) & (x1'=0); + [time] s1=5 & x1 (x1'=min(x1+1,168)); + // snd_req + // do not use x1 until reset (in state 0 or in state 1) so do not need to increase x1 + // also can set x1 to 0 upon entering this state + [rec_req21] s1=6 -> (s1'=0); + [rec_ack21] s1=6 -> (s1'=8); + [time] s1=6 -> (s1'=s1); + // almost root (immediate) + // loop in final states to remove deadlock + [] s1=7 & s2=8 -> (s1'=s1); + [] s1=8 & s2=7 -> (s1'=s1); + [time] s1=7 -> (s1'=s1); + [time] s1=8 -> (s1'=s1); + +endmodule + +// construct remaining automata through renaming +module wire21=wire12[w12=w21, y1=z1, y2=z2, + snd_req12=snd_req21, snd_idle12=snd_idle21, snd_ack12=snd_ack21, + rec_req12=rec_req21, rec_idle12=rec_idle21, rec_ack12=rec_ack21] +endmodule +module node2=node1[s1=s2, s2=s1, x1=x2, fast1=fast2, slow1=slow2, + rec_req21=rec_req12, rec_idle21=rec_idle12, rec_ack21=rec_ack12, + snd_req12=snd_req21, snd_idle12=snd_idle21, snd_ack12=snd_ack21] +endmodule + +// labels +label "done" = (s1=8 & s2=7) | (s1=7 & s2=8); + +// reward structures + +// time +rewards "time" + [time] true : 1; +endrewards + +// time nodes sending +rewards "time_sending" + [time] (w12>0 | w21>0) : 1; +endrewards diff --git a/examples/pmdp/firewire/firewire.prop b/examples/pmdp/firewire/firewire.prop new file mode 100644 index 000000000..2c1278d1d --- /dev/null +++ b/examples/pmdp/firewire/firewire.prop @@ -0,0 +1,4 @@ +Pmin=?[ F (s1=8 & s2=7) ] +//R{"time"}min=? [ F "done" ] +//R{"time"}max=? [ F "done" ] +//R{"time_sending"}max=? [ F "done" ] diff --git a/examples/pmdp/zeroconf/zeroconf.nm b/examples/pmdp/zeroconf/zeroconf.nm new file mode 100644 index 000000000..9c71181f2 --- /dev/null +++ b/examples/pmdp/zeroconf/zeroconf.nm @@ -0,0 +1,258 @@ +// IPv4: PTA model with digitial clocks +// one concrete host attempting to choose an ip address +// when a number of (abstract) hosts have already got ip addresses +// gxn/dxp/jzs 02/05/03 + +// model is an mdp +mdp + +// reset or noreset model +const bool reset=false; + +//------------------------------------------------------------- + +// we suppose that +// - the abstract hosts have already picked their addresses +// and always defend their addresses +// - the concrete host never picks the same ip address twice +// (this can happen only with a verys small probability) + +// under these assumptions we do not need message types because: +// 1) since messages to the concrete host will never be a probe, +// this host will react to all messages in the same way +// 2) since the abstract hosts always defend their addresses, +// all messages from the host will get an arp reply if the ip matches + +// following from the above assumptions we require only three abstract IP addresses +// (0,1 and 2) which correspond to the following sets of IP addresses: + +// 0 - the IP addresses of the abstract hosts which the concrete host +// previously tried to configure +// 1 - an IP address of an abstract host which the concrete host is +// currently trying to configure +// 2 - a fresh IP address which the concrete host is currently trying to configure + +// if the host picks an address that is being used it may end up picking another ip address +// in which case there may still be messages corresponding to the old ip address +// to be sent both from and to the host which the host should now disregard +// (since it will never pick the same ip address) + +// to deal with this situation: when a host picks a new ip address we reconfigure the +// messages that are still be be sent or are being sent by changing the ip address to 0 +// (an old ip address of the host) + +// all the messages from the abstract hosts for the 'old' address (in fact the +// set of old addresses since it may have started again more than once) +// can arrive in any order since they are equivalent to the host - it ignores then all + +// also the messages for the old and new address will come from different hosts +// (the ones with that ip address) which we model by allowing them to arrive in any order +// i.e. not neccessarily in the order they where sent + +//------------------------------------------------------------- + + +//------------------------------------------------------------- +// VARIABLES +//const int N; // number of abstract hosts +const int K; // number of probes to send +const double loss; // probability of message loss + +// PROBABILITIES +const double old; //=N/65024; // probability pick an ip address being used +const double new = (1-old); // probability pick a new ip address + +// TIMING CONSTANTS +const int CONSEC = 2; // time interval between sending consecutive probles +const int TRANSTIME = 1; // upper bound on transmission time delay +const int LONGWAIT = 60; // minimum time delay after a high number of address collisions +const int DEFEND = 10; + +const int TIME_MAX_X = 60; // max value of clock x +const int TIME_MAX_Y = 10; // max value of clock y +const int TIME_MAX_Z = 1; // max value of clock z + +// OTHER CONSTANTS +const int MAXCOLL = 10; // maximum number of collisions before long wait +// size of buffers for other hosts +const int B0 = 20; // buffer size for one abstract host +const int B1 = 8; // buffer sizes for all abstract hosts + +//------------------------------------------------------------- +// ENVIRONMENT - models: medium, output buffer of concrete host and all other hosts +module environment + + // buffer of concrete host + b_ip7 : [0..2]; // ip address of message in buffer position 8 + b_ip6 : [0..2]; // ip address of message in buffer position 7 + b_ip5 : [0..2]; // ip address of message in buffer position 6 + b_ip4 : [0..2]; // ip address of message in buffer position 5 + b_ip3 : [0..2]; // ip address of message in buffer position 4 + b_ip2 : [0..2]; // ip address of message in buffer position 3 + b_ip1 : [0..2]; // ip address of message in buffer position 2 + b_ip0 : [0..2]; // ip address of message in buffer position 1 + n : [0..8]; // number of places in the buffer used (from host) + + // messages to be sent from abstract hosts to concrete host + n0 : [0..B0]; // number of messages which do not have the host's current ip address + n1 : [0..B1]; // number of messages which have the host's current ip address + + b : [0..2]; // local state + // 0 - idle + // 1 - sending message from concrete host + // 2 - sending message from abstract host + + z : [0..1]; // clock of environment (needed for the time to send a message) + + ip_mess : [0..2]; // ip in the current message being sent + // 0 - different from concrete host + // 1 - same as the concrete host and in use + // 2 - same as the concrete host and not in use + + // RESET/RECONFIG: when host is about to choose new ip address + // suppose that the host cannot choose the same ip address + // (since happens with very small probability). + // Therefore all messages will have a different ip address, + // i.e. all n1 messages become n0 ones. + // Note this include any message currently being sent (ip is set to zero 0) + [reset] true -> (n1'=0) & (n0'=min(B0,n0+n1)) // abstract buffers + & (ip_mess'=0) // message being set + & (n'=(reset)?0:n) // concrete buffer (remove this update to get NO_RESET model) + & (b_ip7'=0) + & (b_ip6'=0) + & (b_ip5'=0) + & (b_ip4'=0) + & (b_ip3'=0) + & (b_ip2'=0) + & (b_ip1'=0) + & (b_ip0'=0); + // note: prevent anything else from happening when reconfiguration needs to take place + + // time passage (only if no messages to send or sending a message) + [time] l>0 & b=0 & n=0 & n0=0 & n1=0 -> (b'=b); // cannot send a message + [time] l>0 & b>0 & z<1 -> (z'=min(z+1,TIME_MAX_Z)); // sending a message + + // get messages to be sent (so message has same ip address as host) + [send] l>0 & n=0 -> (b_ip0'=ip) & (n'=n+1); + [send] l>0 & n=1 -> (b_ip1'=ip) & (n'=n+1); + [send] l>0 & n=2 -> (b_ip2'=ip) & (n'=n+1); + [send] l>0 & n=3 -> (b_ip3'=ip) & (n'=n+1); + [send] l>0 & n=4 -> (b_ip4'=ip) & (n'=n+1); + [send] l>0 & n=5 -> (b_ip5'=ip) & (n'=n+1); + [send] l>0 & n=6 -> (b_ip6'=ip) & (n'=n+1); + [send] l>0 & n=7 -> (b_ip7'=ip) & (n'=n+1); + [send] l>0 & n=8 -> (n'=n); // buffer full so lose message + + // start sending message from host + [] l>0 & b=0 & n>0 -> (1-loss) : (b'=1) & (ip_mess'=b_ip0) + & (n'=n-1) + & (b_ip7'=0) + & (b_ip6'=b_ip7) + & (b_ip5'=b_ip6) + & (b_ip4'=b_ip5) + & (b_ip3'=b_ip4) + & (b_ip2'=b_ip3) + & (b_ip1'=b_ip2) + & (b_ip0'=b_ip1) // send message + + loss : (n'=n-1) + & (b_ip7'=0) + & (b_ip6'=b_ip7) + & (b_ip5'=b_ip6) + & (b_ip4'=b_ip5) + & (b_ip3'=b_ip4) + & (b_ip2'=b_ip3) + & (b_ip1'=b_ip2) + & (b_ip0'=b_ip1); // lose message + + // start sending message to host + [] l>0 & b=0 & n0>0 -> (1-loss) : (b'=2) & (ip_mess'=0) & (n0'=n0-1) + loss : (n0'=n0-1); // different ip + [] l>0 & b=0 & n1>0 -> (1-loss) : (b'=2) & (ip_mess'=1) & (n1'=n1-1) + loss : (n1'=n1-1); // same ip + + // finish sending message from host + [] l>0 & b=1 & ip_mess=0 -> (b'=0) & (z'=0) & (n0'=min(n0+1,B0)) & (ip_mess'=0); + [] l>0 & b=1 & ip_mess=1 -> (b'=0) & (z'=0) & (n1'=min(n1+1,B1)) & (ip_mess'=0); + [] l>0 & b=1 & ip_mess=2 -> (b'=0) & (z'=0) & (ip_mess'=0); + + // finish sending message to host + [rec] l>0 & b=2 -> (b'=0) & (z'=0) & (ip_mess'=0); + +endmodule + +//------------------------------------------------------------- +// CONCRETE HOST +module host0 + + x : [0..TIME_MAX_X]; // first clock of the host + y : [0..TIME_MAX_Y]; // second clock of the host + + coll : [0..MAXCOLL]; // number of address collisions + probes : [0..K]; // counter (number of probes sent) + mess : [0..1]; // need to send a message or not + defend : [0..1]; // defend (if =1, try to defend IP address) + + ip : [1..2]; // ip address (1 - in use & 2 - fresh) + + l : [0..4] init 1; // location + // 0 : RECONFIGURE + // 1 : RANDOM + // 2 : WAITSP + // 3 : WAITSG + // 4 : USE + + // RECONFIGURE + [reset] l=0 -> (l'=1); + + // RANDOM (choose IP address) + [rec] (l=1) -> 1: true; // get message (ignore since have no ip address) + // small number of collisions (choose straight away) + [] l=1 & coll 1/3*old : (l'=2) & (ip'=1) & (x'=0) + + 1/3*old : (l'=2) & (ip'=1) & (x'=1) + + 1/3*old : (l'=2) & (ip'=1) & (x'=2) + + 1/3*new : (l'=2) & (ip'=2) & (x'=0) + + 1/3*new : (l'=2) & (ip'=2) & (x'=1) + + 1/3*new : (l'=2) & (ip'=2) & (x'=2); + // large number of collisions: (wait for LONGWAIT) + [time] l=1 & coll=MAXCOLL & x (x'=min(x+1,TIME_MAX_X)); + [] l=1 & coll=MAXCOLL & x=LONGWAIT -> 1/3*old : (l'=2) & (ip'=1) & (x'=0) + + 1/3*old : (l'=2) & (ip'=1) & (x'=1) + + 1/3*old : (l'=2) & (ip'=1) & (x'=2) + + 1/3*new : (l'=2) & (ip'=2) & (x'=0) + + 1/3*new : (l'=2) & (ip'=2) & (x'=1) + + 1/3*new : (l'=2) & (ip'=2) & (x'=2); + + // WAITSP + // let time pass + [time] l=2 & x<2 -> (x'=min(x+1,2)); + // send probe + [send] l=2 & x=2 & probes (x'=0) & (probes'=probes+1); + // sent K probes and waited 2 seconds + [] l=2 & x=2 & probes=K -> (l'=3) & (probes'=0) & (coll'=0) & (x'=0); + // get message and ip does not match: ignore + [rec] l=2 & ip_mess!=ip -> (l'=l); + // get a message with matching ip: reconfigure + [rec] l=2 & ip_mess=ip -> (l'=0) & (coll'=min(coll+1,MAXCOLL)) & (x'=0) & (probes'=0); + + // WAITSG (sends two gratuitious arp probes) + // time passage + [time] l=3 & mess=0 & defend=0 & x (x'=min(x+1,TIME_MAX_X)); + [time] l=3 & mess=0 & defend=1 & x (x'=min(x+1,TIME_MAX_X)) & (y'=min(y+1,DEFEND)); + + // receive message and same ip: defend + [rec] l=3 & mess=0 & ip_mess=ip & (defend=0 | y>=DEFEND) -> (defend'=1) & (mess'=1) & (y'=0); + // receive message and same ip: defer + [rec] l=3 & mess=0 & ip_mess=ip & (defend=0 | y (l'=0) & (probes'=0) & (defend'=0) & (x'=0) & (y'=0); + // receive message and different ip + [rec] l=3 & mess=0 & ip_mess!=ip -> (l'=l); + + + // send probe reply or message for defence + [send] l=3 & mess=1 -> (mess'=0); + // send first gratuitous arp message + [send] l=3 & mess=0 & x=CONSEC & probes<1 -> (x'=0) & (probes'=probes+1); + // send second gratuitous arp message (move to use) + [send] l=3 & mess=0 & x=CONSEC & probes=1 -> (l'=4) & (x'=0) & (y'=0) & (probes'=0); + + // USE (only interested in reaching this state so do not need to add anything here) + [] l=4 -> 1 : true; + +endmodule diff --git a/examples/pmdp/zeroconf/zeroconf.prop b/examples/pmdp/zeroconf/zeroconf.prop new file mode 100644 index 000000000..43903b9f4 --- /dev/null +++ b/examples/pmdp/zeroconf/zeroconf.prop @@ -0,0 +1,2 @@ +Pmin=? [ F (l=4 & ip=1) ] +Pmax=? [ F (l=4 & ip=1) ] \ No newline at end of file diff --git a/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.h b/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.h index 692a6be57..eaeaed48e 100644 --- a/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.h +++ b/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.h @@ -9,8 +9,17 @@ namespace storm { namespace modelchecker { + //forward declaration of friend class + namespace region { + template + class SparseDtmcRegionModelChecker; + } + template class SparseDtmcEliminationModelChecker : public SparsePropositionalModelChecker { + + template friend class storm::modelchecker::region::SparseDtmcRegionModelChecker; + public: typedef typename SparseDtmcModelType::ValueType ValueType; typedef typename SparseDtmcModelType::RewardModelType RewardModelType; diff --git a/src/modelchecker/region/SparseDtmcRegionModelChecker.cpp b/src/modelchecker/region/SparseDtmcRegionModelChecker.cpp index 26e60b357..2f224279a 100644 --- a/src/modelchecker/region/SparseDtmcRegionModelChecker.cpp +++ b/src/modelchecker/region/SparseDtmcRegionModelChecker.cpp @@ -402,16 +402,18 @@ namespace storm { //now compute the functions using methods from elimination model checker storm::storage::BitVector newInitialStates = simpleModel.getInitialStates() % maybeStates; storm::storage::BitVector phiStates(simpleModel.getNumberOfStates(), true); - boost::optional> stateRewards; + std::vector values; if(this->isComputeRewards()){ - stateRewards = simpleModel.getUniqueRewardModel()->second.getTotalRewardVector(maybeStates.getNumberOfSetBits(), simpleModel.getTransitionMatrix(), maybeStates); + values = simpleModel.getUniqueRewardModel()->second.getTotalRewardVector(maybeStates.getNumberOfSetBits(), simpleModel.getTransitionMatrix(), maybeStates); + } else { + values = oneStepProbabilities; } // storm::modelchecker::SparseDtmcEliminationModelChecker> eliminationModelChecker(simpleModel); // std::vector statePriorities = eliminationModelChecker.getStatePriorities(forwardTransitions,backwardTransitions,newInitialStates,oneStepProbabilities); // this->reachabilityFunction=std::make_shared(eliminationModelChecker.computeReachabilityValue(forwardTransitions, oneStepProbabilities, backwardTransitions, newInitialStates , true, phiStates, simpleModel.getStates("target"), stateRewards, statePriorities)); - // std::vector reachFuncVector = storm::modelchecker::SparseDtmcEliminationModelChecker>::computeReachabilityValues( - // forwardTransitions, oneStepProbabilities, backwardTransitions, newInitialStates , true, phiStates, simpleModel.getStates("target"), oneStepProbabilities); - // this->reachabilityFunction=std::make_shared(std::move(reachFuncVector[*newInitialStates.begin()])); + std::vector reachFuncVector = storm::modelchecker::SparseDtmcEliminationModelChecker>::computeReachabilityValues( + forwardTransitions, values, backwardTransitions, newInitialStates , true, phiStates, simpleModel.getStates("target"), oneStepProbabilities); + this->reachabilityFunction=std::make_shared(std::move(reachFuncVector[*simpleModel.getInitialStates().begin()])); /* std::string funcStr = " (/ " + this->reachabilityFunction->nominator().toString(false, true) + " " + this->reachabilityFunction->denominator().toString(false, true) +