From dc8921037e9247d1887cf1d855390d8cf656769d Mon Sep 17 00:00:00 2001 From: dehnert Date: Wed, 16 Apr 2014 18:56:04 +0200 Subject: [PATCH 1/5] Added missing test inputs. Former-commit-id: 537971f3659506aaf496406e00ed78e5aa26bc97 --- test/functional/parser/prism/coin2.nm | 60 +++++ test/functional/parser/prism/crowds5_5.pm | 69 ++++++ test/functional/parser/prism/csma2_2.nm | 130 +++++++++++ test/functional/parser/prism/die.pm | 24 ++ test/functional/parser/prism/firewire.nm | 170 ++++++++++++++ test/functional/parser/prism/leader3.nm | 96 ++++++++ test/functional/parser/prism/leader3_5.pm | 85 +++++++ test/functional/parser/prism/two_dice.nm | 40 ++++ test/functional/parser/prism/wlan0_collide.nm | 219 ++++++++++++++++++ 9 files changed, 893 insertions(+) create mode 100644 test/functional/parser/prism/coin2.nm create mode 100644 test/functional/parser/prism/crowds5_5.pm create mode 100644 test/functional/parser/prism/csma2_2.nm create mode 100644 test/functional/parser/prism/die.pm create mode 100644 test/functional/parser/prism/firewire.nm create mode 100644 test/functional/parser/prism/leader3.nm create mode 100644 test/functional/parser/prism/leader3_5.pm create mode 100644 test/functional/parser/prism/two_dice.nm create mode 100644 test/functional/parser/prism/wlan0_collide.nm diff --git a/test/functional/parser/prism/coin2.nm b/test/functional/parser/prism/coin2.nm new file mode 100644 index 000000000..a08bb8741 --- /dev/null +++ b/test/functional/parser/prism/coin2.nm @@ -0,0 +1,60 @@ +// COIN FLIPPING PROTOCOL FOR POLYNOMIAL RANDOMIZED CONSENSUS [AH90] +// gxn/dxp 20/11/00 + +mdp + +// constants +const int N=2; +const int K; +const int range = 2*(K+1)*N; +const int counter_init = (K+1)*N; +const int left = N; +const int right = 2*(K+1)*N - N; + +// shared coin +global counter : [0..range] init counter_init; + +module process1 + + // program counter + pc1 : [0..3]; + // 0 - flip + // 1 - write + // 2 - check + // 3 - finished + + // local coin + coin1 : [0..1]; + + // flip coin + [] (pc1=0) -> 0.5 : (coin1'=0) & (pc1'=1) + 0.5 : (coin1'=1) & (pc1'=1); + // write tails -1 (reset coin to add regularity) + [] (pc1=1) & (coin1=0) & (counter>0) -> 1 : (counter'=counter-1) & (pc1'=2) & (coin1'=0); + // write heads +1 (reset coin to add regularity) + [] (pc1=1) & (coin1=1) & (counter 1 : (counter'=counter+1) & (pc1'=2) & (coin1'=0); + // check + // decide tails + [] (pc1=2) & (counter<=left) -> 1 : (pc1'=3) & (coin1'=0); + // decide heads + [] (pc1=2) & (counter>=right) -> 1 : (pc1'=3) & (coin1'=1); + // flip again + [] (pc1=2) & (counter>left) & (counter 1 : (pc1'=0); + // loop (all loop together when done) + [done] (pc1=3) -> 1 : (pc1'=3); + +endmodule + +// construct remaining processes through renaming +module process2 = process1[pc1=pc2,coin1=coin2] endmodule + +// labels +label "finished" = pc1=3 & pc2=3 ; +label "all_coins_equal_0" = coin1=0 & coin2=0 ; +label "all_coins_equal_1" = coin1=1 & coin2=1 ; +label "agree" = coin1=coin2 ; + +// rewards +rewards "steps" + true : 1; +endrewards + diff --git a/test/functional/parser/prism/crowds5_5.pm b/test/functional/parser/prism/crowds5_5.pm new file mode 100644 index 000000000..60bdaa7ea --- /dev/null +++ b/test/functional/parser/prism/crowds5_5.pm @@ -0,0 +1,69 @@ +dtmc + +// probability of forwarding +const double PF = 0.8; +const double notPF = .2; // must be 1-PF +// probability that a crowd member is bad +const double badC = .167; + // probability that a crowd member is good +const double goodC = 0.833; +// Total number of protocol runs to analyze +const int TotalRuns = 5; +// size of the crowd +const int CrowdSize = 5; + +module crowds + // protocol phase + phase: [0..4] init 0; + + // crowd member good (or bad) + good: bool init false; + + // number of protocol runs + runCount: [0..TotalRuns] init 0; + + // observe_i is the number of times the attacker observed crowd member i + observe0: [0..TotalRuns] init 0; + + observe1: [0..TotalRuns] init 0; + + observe2: [0..TotalRuns] init 0; + + observe3: [0..TotalRuns] init 0; + + observe4: [0..TotalRuns] init 0; + + // the last seen crowd member + lastSeen: [0..CrowdSize - 1] init 0; + + // get the protocol started + [] phase=0 & runCount 1: (phase'=1) & (runCount'=runCount+1) & (lastSeen'=0); + + // decide whether crowd member is good or bad according to given probabilities + [] phase=1 -> goodC : (phase'=2) & (good'=true) + badC : (phase'=2) & (good'=false); + + // if the current member is a good member, update the last seen index (chosen uniformly) + [] phase=2 & good -> 1/5 : (lastSeen'=0) & (phase'=3) + 1/5 : (lastSeen'=1) & (phase'=3) + 1/5 : (lastSeen'=2) & (phase'=3) + 1/5 : (lastSeen'=3) & (phase'=3) + 1/5 : (lastSeen'=4) & (phase'=3); + + // if the current member is a bad member, record the most recently seen index + [] phase=2 & !good & lastSeen=0 & observe0 < TotalRuns -> 1: (observe0'=observe0+1) & (phase'=4); + [] phase=2 & !good & lastSeen=1 & observe1 < TotalRuns -> 1: (observe1'=observe1+1) & (phase'=4); + [] phase=2 & !good & lastSeen=2 & observe2 < TotalRuns -> 1: (observe2'=observe2+1) & (phase'=4); + [] phase=2 & !good & lastSeen=3 & observe3 < TotalRuns -> 1: (observe3'=observe3+1) & (phase'=4); + [] phase=2 & !good & lastSeen=4 & observe4 < TotalRuns -> 1: (observe4'=observe4+1) & (phase'=4); + + // good crowd members forward with probability PF and deliver otherwise + [] phase=3 -> PF : (phase'=1) + notPF : (phase'=4); + + // deliver the message and start over + [] phase=4 -> 1: (phase'=0); + +endmodule + +label "observe0Greater1" = observe0>1; +label "observe1Greater1" = observe1>1; +label "observe2Greater1" = observe2>1; +label "observe3Greater1" = observe3>1; +label "observe4Greater1" = observe4>1; +label "observeIGreater1" = observe1>1|observe2>1|observe3>1|observe4>1; +label "observeOnlyTrueSender" = observe0>1&observe1<=1 & observe2<=1 & observe3<=1 & observe4<=1; diff --git a/test/functional/parser/prism/csma2_2.nm b/test/functional/parser/prism/csma2_2.nm new file mode 100644 index 000000000..18ec5c897 --- /dev/null +++ b/test/functional/parser/prism/csma2_2.nm @@ -0,0 +1,130 @@ +// CSMA/CD protocol - probabilistic version of kronos model (3 stations) +// gxn/dxp 04/12/01 + +mdp + +// note made changes since cannot have strict inequalities +// in digital clocks approach and suppose a station only sends one message + +// simplified parameters scaled +const int sigma=1; // time for messages to propagate along the bus +const int lambda=30; // time to send a message + +// actual parameters +const int N = 2; // number of processes +const int K = 2; // exponential backoff limit +const int slot = 2*sigma; // length of slot +// const int M = floor(pow(2, K))-1 ; // max number of slots to wait +const int M = 3 ; // max number of slots to wait +//const int lambda=782; +//const int sigma=26; + +// formula min_backoff_after_success = min(s1=4?cd1:K+1,s2=4?cd2:K+1); +// formula min_collisions = min(cd1,cd2); +// formula max_collisions = max(cd1,cd2); + +//---------------------------------------------------------------------------------------------------------------------------- +// the bus +module bus + + b : [0..2]; + // b=0 - idle + // b=1 - active + // b=2 - collision + + // clocks of bus + y1 : [0..sigma+1]; // time since first send (used find time until channel sensed busy) + y2 : [0..sigma+1]; // time since second send (used to find time until collision detected) + + // a sender sends (ok - no other message being sent) + [send1] (b=0) -> (b'=1); + [send2] (b=0) -> (b'=1); + + // a sender sends (bus busy - collision) + [send1] (b=1|b=2) & (y1 (b'=2); + [send2] (b=1|b=2) & (y1 (b'=2); + + // finish sending + [end1] (b=1) -> (b'=0) & (y1'=0); + [end2] (b=1) -> (b'=0) & (y1'=0); + + // bus busy + [busy1] (b=1|b=2) & (y1>=sigma) -> (b'=b); + [busy2] (b=1|b=2) & (y1>=sigma) -> (b'=b); + + // collision detected + [cd] (b=2) & (y2<=sigma) -> (b'=0) & (y1'=0) & (y2'=0); + + // time passage + [time] (b=0) -> (y1'=0); // value of y1/y2 does not matter in state 0 + [time] (b=1) -> (y1'=min(y1+1,sigma+1)); // no invariant in state 1 + [time] (b=2) & (y2 (y1'=min(y1+1,sigma+1)) & (y2'=min(y2+1,sigma+1)); // invariant in state 2 (time until collision detected) + +endmodule + +//---------------------------------------------------------------------------------------------------------------------------- +// model of first sender +module station1 + + // LOCAL STATE + s1 : [0..5]; + // s1=0 - initial state + // s1=1 - transmit + // s1=2 - collision (set backoff) + // s1=3 - wait (bus busy) + // s1=4 - successfully sent + + // LOCAL CLOCK + x1 : [0..max(lambda,slot)]; + + // BACKOFF COUNTER (number of slots to wait) + bc1 : [0..M]; + + // COLLISION COUNTER + cd1 : [0..K]; + + // start sending + [send1] (s1=0) -> (s1'=1) & (x1'=0); // start sending + [busy1] (s1=0) -> (s1'=2) & (x1'=0) & (cd1'=min(K,cd1+1)); // detects channel is busy so go into backoff + + // transmitting + [time] (s1=1) & (x1 (x1'=min(x1+1,lambda)); // let time pass + [end1] (s1=1) & (x1=lambda) -> (s1'=4) & (x1'=0); // finished + [cd] (s1=1) -> (s1'=2) & (x1'=0) & (cd1'=min(K,cd1+1)); // collision detected (increment backoff counter) + [cd] !(s1=1) -> (s1'=s1); // add loop for collision detection when not important + + // set backoff (no time can pass in this state) + // probability depends on which transmission this is (cd1) + [] s1=2 & cd1=1 -> 1/2 : (s1'=3) & (bc1'=0) + 1/2 : (s1'=3) & (bc1'=1) ; + [] s1=2 & cd1=2 -> 1/4 : (s1'=3) & (bc1'=0) + 1/4 : (s1'=3) & (bc1'=1) + 1/4 : (s1'=3) & (bc1'=2) + 1/4 : (s1'=3) & (bc1'=3) ; + + // wait until backoff counter reaches 0 then send again + [time] (s1=3) & (x1 (x1'=x1+1); // let time pass (in slot) + [time] (s1=3) & (x1=slot) & (bc1>0) -> (x1'=1) & (bc1'=bc1-1); // let time pass (move slots) + [send1] (s1=3) & (x1=slot) & (bc1=0) -> (s1'=1) & (x1'=0); // finished backoff (bus appears free) + [busy1] (s1=3) & (x1=slot) & (bc1=0) -> (s1'=2) & (x1'=0) & (cd1'=min(K,cd1+1)); // finished backoff (bus busy) + + // once finished nothing matters + [time] (s1>=4) -> (x1'=0); + +endmodule + +//---------------------------------------------------------------------------------------------------------------------------- + +// construct further stations through renaming +module station2=station1[s1=s2,x1=x2,cd1=cd2,bc1=bc2,send1=send2,busy1=busy2,end1=end2] endmodule + +//---------------------------------------------------------------------------------------------------------------------------- + +// reward structure for expected time +rewards "time" + [time] true : 1; +endrewards + +//---------------------------------------------------------------------------------------------------------------------------- + +// labels/formulae +label "all_delivered" = s1=4&s2=4; +label "one_delivered" = s1=4|s2=4; +label "collision_max_backoff" = (cd1=K & s1=1 & b=2)|(cd2=K & s2=1 & b=2); + diff --git a/test/functional/parser/prism/die.pm b/test/functional/parser/prism/die.pm new file mode 100644 index 000000000..700951a05 --- /dev/null +++ b/test/functional/parser/prism/die.pm @@ -0,0 +1,24 @@ +// Knuth's model of a fair die using only fair coins +dtmc + +module die + + // local state + s : [0..7] init 0; + // value of the dice + d : [0..6] init 0; + + [] s=0 -> 0.5 : (s'=1) + 0.5 : (s'=2); + [] s=1 -> 0.5 : (s'=3) + 0.5 : (s'=4); + [] s=2 -> 0.5 : (s'=5) + 0.5 : (s'=6); + [] s=3 -> 0.5 : (s'=1) + 0.5 : (s'=7) & (d'=1); + [] s=4 -> 0.5 : (s'=7) & (d'=2) + 0.5 : (s'=7) & (d'=3); + [] s=5 -> 0.5 : (s'=7) & (d'=4) + 0.5 : (s'=7) & (d'=5); + [] s=6 -> 0.5 : (s'=2) + 0.5 : (s'=7) & (d'=6); + [] s=7 -> 1: (s'=7); + +endmodule + +rewards "coin_flips" + [] s<7 : 1; +endrewards diff --git a/test/functional/parser/prism/firewire.nm b/test/functional/parser/prism/firewire.nm new file mode 100644 index 000000000..26fa210b4 --- /dev/null +++ b/test/functional/parser/prism/firewire.nm @@ -0,0 +1,170 @@ +// 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 fast; +const double slow=1-fast; + +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 -> fast : (s1'=2) & (x1'=0) + slow : (s1'=3) & (x1'=0); + [rec_idle21] s1=0 -> (s1'=1); + // rec_idle immediate state) + [snd_idle12] s1=1 -> fast : (s1'=4) & (x1'=0) + slow : (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, + 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 + +// reward structures +// time +rewards "time" + [time] true : 1; +endrewards +// time nodes sending +rewards "time_sending" + [time] (w12>0 | w21>0) : 1; +endrewards + +label "elected" = ((s1=8) & (s2=7)) | ((s1=7) & (s2=8)); \ No newline at end of file diff --git a/test/functional/parser/prism/leader3.nm b/test/functional/parser/prism/leader3.nm new file mode 100644 index 000000000..5a8cd34b5 --- /dev/null +++ b/test/functional/parser/prism/leader3.nm @@ -0,0 +1,96 @@ +// asynchronous leader election +// 4 processes +// gxn/dxp 29/01/01 + +mdp + +const int N = 3; // number of processes + +//---------------------------------------------------------------------------------------------------------------------------- +module process1 + + // COUNTER + c1 : [0..3-1]; + + // STATES + s1 : [0..4]; + // 0 make choice + // 1 have not received neighbours choice + // 2 active + // 3 inactive + // 4 leader + + // PREFERENCE + p1 : [0..1]; + + // VARIABLES FOR SENDING AND RECEIVING + receive1 : [0..2]; + // not received anything + // received choice + // received counter + sent1 : [0..2]; + // not send anything + // sent choice + // sent counter + + // pick value + [] (s1=0) -> 0.5 : (s1'=1) & (p1'=0) + 0.5 : (s1'=1) & (p1'=1); + + // send preference + [p12] (s1=1) & (sent1=0) -> (sent1'=1); + // receive preference + // stay active + [p31] (s1=1) & (receive1=0) & !( (p1=0) & (p3=1) ) -> (s1'=2) & (receive1'=1); + // become inactive + [p31] (s1=1) & (receive1=0) & (p1=0) & (p3=1) -> (s1'=3) & (receive1'=1); + + // send preference (can now reset preference) + [p12] (s1=2) & (sent1=0) -> (sent1'=1) & (p1'=0); + // send counter (already sent preference) + // not received counter yet + [c12] (s1=2) & (sent1=1) & (receive1=1) -> (sent1'=2); + // received counter (pick again) + [c12] (s1=2) & (sent1=1) & (receive1=2) -> (s1'=0) & (p1'=0) & (c1'=0) & (sent1'=0) & (receive1'=0); + + // receive counter and not sent yet (note in this case do not pass it on as will send own counter) + [c31] (s1=2) & (receive1=1) & (sent1<2) -> (receive1'=2); + // receive counter and sent counter + // only active process (decide) + [c31] (s1=2) & (receive1=1) & (sent1=2) & (c3=N-1) -> (s1'=4) & (p1'=0) & (c1'=0) & (sent1'=0) & (receive1'=0); + // other active process (pick again) + [c31] (s1=2) & (receive1=1) & (sent1=2) & (c3 (s1'=0) & (p1'=0) & (c1'=0) & (sent1'=0) & (receive1'=0); + + // send preference (must have received preference) and can now reset + [p12] (s1=3) & (receive1>0) & (sent1=0) -> (sent1'=1) & (p1'=0); + // send counter (must have received counter first) and can now reset + [c12] (s1=3) & (receive1=2) & (sent1=1) -> (s1'=3) & (p1'=0) & (c1'=0) & (sent1'=0) & (receive1'=0); + + // receive preference + [p31] (s1=3) & (receive1=0) -> (p1'=p3) & (receive1'=1); + // receive counter + [c31] (s1=3) & (receive1=1) & (c3 (c1'=c3+1) & (receive1'=2); + + // done + [done] (s1=4) -> (s1'=s1); + // add loop for processes who are inactive + [done] (s1=3) -> (s1'=s1); + +endmodule + +//---------------------------------------------------------------------------------------------------------------------------- + +// construct further stations through renaming +module process2=process1[s1=s2,p1=p2,c1=c2,sent1=sent2,receive1=receive2,p12=p23,p31=p12,c12=c23,c31=c12,p3=p1,c3=c1] endmodule +module process3=process1[s1=s3,p1=p3,c1=c3,sent1=sent3,receive1=receive3,p12=p31,p31=p23,c12=c31,c31=c23,p3=p2,c3=c2] endmodule + +//---------------------------------------------------------------------------------------------------------------------------- + +// reward - expected number of rounds (equals the number of times a process receives a counter) +rewards "name" + [c12] true : 1; +endrewards + +//---------------------------------------------------------------------------------------------------------------------------- +formula leaders = (s1=4?1:0)+(s2=4?1:0)+(s3=4?1:0); +label "elected" = s1=4|s2=4|s3=4; + diff --git a/test/functional/parser/prism/leader3_5.pm b/test/functional/parser/prism/leader3_5.pm new file mode 100644 index 000000000..0703e733d --- /dev/null +++ b/test/functional/parser/prism/leader3_5.pm @@ -0,0 +1,85 @@ +// synchronous leader election protocol (itai & Rodeh) +// dxp/gxn 25/01/01 + +dtmc + +// CONSTANTS +const int N = 3; // number of processes +const int K = 5; // range of probabilistic choice + +// counter module used to count the number of processes that have been read +// and to know when a process has decided +module counter + + // counter (c=i means process j reading process (i-1)+j next) + c : [1..N-1]; + + // reading + [read] c 1:(c'=c+1); + // finished reading + [read] c=N-1 -> 1:(c'=c); + //decide + [done] u1|u2|u3 -> 1:(c'=c); + // pick again reset counter + [retry] !(u1|u2|u3) -> 1:(c'=1); + // loop (when finished to avoid deadlocks) + [loop] s1=3 -> 1:(c'=c); + +endmodule + +// processes form a ring and suppose: +// process 1 reads process 2 +// process 2 reads process 3 +// process 3 reads process 1 +module process1 + + // local state + s1 : [0..3]; + // s1=0 make random choice + // s1=1 reading + // s1=2 deciding + // s1=3 finished + + // has a unique id so far (initially true) + u1 : bool; + + // value to be sent to next process in the ring (initially sets this to its own value) + v1 : [0..K-1]; + + // random choice + p1 : [0..K-1]; + + // pick value + [pick] s1=0 -> 1/K : (s1'=1) & (p1'=0) & (v1'=0) & (u1'=true) + + 1/K : (s1'=1) & (p1'=1) & (v1'=1) & (u1'=true) + + 1/K : (s1'=1) & (p1'=2) & (v1'=2) & (u1'=true) + + 1/K : (s1'=1) & (p1'=3) & (v1'=3) & (u1'=true) + + 1/K : (s1'=1) & (p1'=4) & (v1'=4) & (u1'=true); + // read + [read] s1=1 & u1 & c 1:(u1'=(p1!=v2)) & (v1'=v2); + [read] s1=1 & !u1 & c 1:(u1'=false) & (v1'=v2) & (p1'=0); + // read and move to decide + [read] s1=1 & u1 & c=N-1 -> 1:(s1'=2) & (u1'=(p1!=v2)) & (v1'=0) & (p1'=0); + [read] s1=1 & !u1 & c=N-1 -> 1:(s1'=2) & (u1'=false) & (v1'=0); + // deciding + // done + [done] s1=2 -> 1:(s1'=3) & (u1'=false) & (v1'=0) & (p1'=0); + //retry + [retry] s1=2 -> 1:(s1'=0) & (u1'=false) & (v1'=0) & (p1'=0); + // loop (when finished to avoid deadlocks) + [loop] s1=3 -> 1:(s1'=3); + +endmodule + +// construct remaining processes through renaming +module process2 = process1 [ s1=s2,p1=p2,v1=v2,u1=u2,v2=v3 ] endmodule +module process3 = process1 [ s1=s3,p1=p3,v1=v3,u1=u3,v2=v1 ] endmodule + +// expected number of rounds +rewards "num_rounds" + [pick] true : 1; +endrewards + +// labels +label "elected" = s1=3&s2=3&s3=3; + diff --git a/test/functional/parser/prism/two_dice.nm b/test/functional/parser/prism/two_dice.nm new file mode 100644 index 000000000..778153138 --- /dev/null +++ b/test/functional/parser/prism/two_dice.nm @@ -0,0 +1,40 @@ +// sum of two dice as the asynchronous parallel composition of +// two copies of Knuth's model of a fair die using only fair coins + +mdp + +module die1 + + // local state + s1 : [0..7] init 0; + // value of the dice + d1 : [0..6] init 0; + + [] s1=0 -> 0.5 : (s1'=1) + 0.5 : (s1'=2); + [] s1=1 -> 0.5 : (s1'=3) + 0.5 : (s1'=4); + [] s1=2 -> 0.5 : (s1'=5) + 0.5 : (s1'=6); + [] s1=3 -> 0.5 : (s1'=1) + 0.5 : (s1'=7) & (d1'=1); + [] s1=4 -> 0.5 : (s1'=7) & (d1'=2) + 0.5 : (s1'=7) & (d1'=3); + [] s1=5 -> 0.5 : (s1'=7) & (d1'=4) + 0.5 : (s1'=7) & (d1'=5); + [] s1=6 -> 0.5 : (s1'=2) + 0.5 : (s1'=7) & (d1'=6); + [] s1=7 & s2=7 -> 1: (s1'=7); +endmodule + +module die2 = die1 [ s1=s2, s2=s1, d1=d2 ] endmodule + +rewards "coinflips" + [] s1<7 | s2<7 : 1; +endrewards + +label "done" = s1=7 & s2=7; +label "two" = s1=7 & s2=7 & d1+d2=2; +label "three" = s1=7 & s2=7 & d1+d2=3; +label "four" = s1=7 & s2=7 & d1+d2=4; +label "five" = s1=7 & s2=7 & d1+d2=5; +label "six" = s1=7 & s2=7 & d1+d2=6; +label "seven" = s1=7 & s2=7 & d1+d2=7; +label "eight" = s1=7 & s2=7 & d1+d2=8; +label "nine" = s1=7 & s2=7 & d1+d2=9; +label "ten" = s1=7 & s2=7 & d1+d2=10; +label "eleven" = s1=7 & s2=7 & d1+d2=11; +label "twelve" = s1=7 & s2=7 & d1+d2=12; diff --git a/test/functional/parser/prism/wlan0_collide.nm b/test/functional/parser/prism/wlan0_collide.nm new file mode 100644 index 000000000..1c14704e5 --- /dev/null +++ b/test/functional/parser/prism/wlan0_collide.nm @@ -0,0 +1,219 @@ +// WLAN PROTOCOL (two stations) +// discrete time model +// gxn/jzs 20/02/02 + +mdp + +// COLLISIONS +const int COL; // maximum number of collisions + +// TIMING CONSTRAINTS +// we have used the FHSS parameters +// then scaled by the value of ASLOTTIME +const int ASLOTTIME = 1; +const int DIFS = 3; // due to scaling can be either 2 or 3 which is modelled by a non-deterministic choice +const int VULN = 1; // due to scaling can be either 0 or 1 which is modelled by a non-deterministic choice +const int TRANS_TIME_MAX; // scaling up +const int TRANS_TIME_MIN = 4; // scaling down +const int ACK_TO = 6; +const int ACK = 4; // due to scaling can be either 3 or 4 which is modelled by a non-deterministic choice +const int SIFS = 1; // due to scaling can be either 0 or 1 which is modelled by a non-deterministic choice +// maximum constant used in timing constraints + 1 +const int TIME_MAX = max(ACK_TO,TRANS_TIME_MAX)+1; + +// CONTENTION WINDOW +// CWMIN =15 & CWMAX =16 +// this means that MAX_BACKOFF IS 2 +const int MAX_BACKOFF = 0; + +//-----------------------------------------------------------------// +// THE MEDIUM/CHANNEL + +// FORMULAE FOR THE CHANNEL +// channel is busy +formula busy = c1>0 | c2>0; +// channel is free +formula free = c1=0 & c2=0; + +module medium + + // number of collisions + col : [0..COL]; + + // medium status + c1 : [0..2]; + c2 : [0..2]; + // ci corresponds to messages associated with station i + // 0 nothing being sent + // 1 being sent correctly + // 2 being sent garbled + + // begin sending message and nothing else currently being sent + [send1] c1=0 & c2=0 -> (c1'=1); + [send2] c2=0 & c1=0 -> (c2'=1); + + // begin sending message and something is already being sent + // in this case both messages become garbled + [send1] c1=0 & c2>0 -> (c1'=2) & (c2'=2) & (col'=min(col+1,COL)); + [send2] c2=0 & c1>0 -> (c1'=2) & (c2'=2) & (col'=min(col+1,COL)); + + // finish sending message + [finish1] c1>0 -> (c1'=0); + [finish2] c2>0 -> (c2'=0); + +endmodule + +//-----------------------------------------------------------------// +// STATION 1 +module station1 + // clock for station 1 + x1 : [0..TIME_MAX]; + + // local state + s1 : [1..12]; + // 1 sense + // 2 wait until free before setting backoff + // 3 wait for DIFS then set slot + // 4 set backoff + // 5 backoff + // 6 wait until free in backoff + // 7 wait for DIFS then resume backoff + // 8 vulnerable + // 9 transmit + // 11 wait for SIFS and then ACK + // 10 wait for ACT_TO + // 12 done + // BACKOFF + // separate into slots + slot1 : [0..1]; + backoff1 : [0..15]; + + // BACKOFF COUNTER + bc1 : [0..1]; + // SENSE + // let time pass + [time] s1=1 & x1 (x1'=min(x1+1,TIME_MAX)); + // ready to transmit + [] s1=1 & (x1=DIFS | x1=DIFS-1) -> (s1'=8) & (x1'=0); + // found channel busy so wait until free + [] s1=1 & busy -> (s1'=2) & (x1'=0); + // WAIT UNTIL FREE BEFORE SETTING BACKOFF + // let time pass (no need for the clock x1 to change) + [time] s1=2 & busy -> (s1'=2); + // find that channel is free so check its free for DIFS before setting backoff + [] s1=2 & free -> (s1'=3); + // WAIT FOR DIFS THEN SET BACKOFF + // let time pass + [time] s1=3 & x1 (x1'=min(x1+1,TIME_MAX)); + // found channel busy so wait until free + [] s1=3 & busy -> (s1'=2) & (x1'=0); + // start backoff first uniformly choose slot + // backoff counter 0 + [] s1=3 & (x1=DIFS | x1=DIFS-1) & bc1=0 -> (s1'=4) & (x1'=0) & (slot1'=0) & (bc1'=min(bc1+1,MAX_BACKOFF)); + // SET BACKOFF (no time can pass) + // chosen slot now set backoff + [] s1=4 -> 1/16 : (s1'=5) & (backoff1'=0 ) + + 1/16 : (s1'=5) & (backoff1'=1 ) + + 1/16 : (s1'=5) & (backoff1'=2 ) + + 1/16 : (s1'=5) & (backoff1'=3 ) + + 1/16 : (s1'=5) & (backoff1'=4 ) + + 1/16 : (s1'=5) & (backoff1'=5 ) + + 1/16 : (s1'=5) & (backoff1'=6 ) + + 1/16 : (s1'=5) & (backoff1'=7 ) + + 1/16 : (s1'=5) & (backoff1'=8 ) + + 1/16 : (s1'=5) & (backoff1'=9 ) + + 1/16 : (s1'=5) & (backoff1'=10) + + 1/16 : (s1'=5) & (backoff1'=11) + + 1/16 : (s1'=5) & (backoff1'=12) + + 1/16 : (s1'=5) & (backoff1'=13) + + 1/16 : (s1'=5) & (backoff1'=14) + + 1/16 : (s1'=5) & (backoff1'=15); + // BACKOFF + // let time pass + [time] s1=5 & x1 (x1'=min(x1+1,TIME_MAX)); + // decrement backoff + [] s1=5 & x1=ASLOTTIME & backoff1>0 -> (s1'=5) & (x1'=0) & (backoff1'=backoff1-1); + [] s1=5 & x1=ASLOTTIME & backoff1=0 & slot1>0 -> (s1'=5) & (x1'=0) & (backoff1'=15) & (slot1'=slot1-1); + // finish backoff + [] s1=5 & x1=ASLOTTIME & backoff1=0 & slot1=0 -> (s1'=8) & (x1'=0); + // found channel busy + [] s1=5 & busy -> (s1'=6) & (x1'=0); + // WAIT UNTIL FREE IN BACKOFF + // let time pass (no need for the clock x1 to change) + [time] s1=6 & busy -> (s1'=6); + // find that channel is free + [] s1=6 & free -> (s1'=7); + + // WAIT FOR DIFS THEN RESUME BACKOFF + // let time pass + [time] s1=7 & x1 (x1'=min(x1+1,TIME_MAX)); + // resume backoff (start again from previous backoff) + [] s1=7 & (x1=DIFS | x1=DIFS-1) -> (s1'=5) & (x1'=0); + // found channel busy + [] s1=7 & busy -> (s1'=6) & (x1'=0); + + // VULNERABLE + // let time pass + [time] s1=8 & x1 (x1'=min(x1+1,TIME_MAX)); + // move to transmit + [send1] s1=8 & (x1=VULN | x1=VULN-1) -> (s1'=9) & (x1'=0); + // TRANSMIT + // let time pass + [time] s1=9 & x1 (x1'=min(x1+1,TIME_MAX)); + // finish transmission successful + [finish1] s1=9 & x1>=TRANS_TIME_MIN & c1=1 -> (s1'=10) & (x1'=0); + // finish transmission garbled + [finish1] s1=9 & x1>=TRANS_TIME_MIN & c1=2 -> (s1'=11) & (x1'=0); + // WAIT FOR SIFS THEN WAIT FOR ACK + + // WAIT FOR SIFS i.e. c1=0 + // check channel and busy: go into backoff + [] s1=10 & c1=0 & x1=0 & busy -> (s1'=2); + // check channel and free: let time pass + [time] s1=10 & c1=0 & x1=0 & free -> (x1'=min(x1+1,TIME_MAX)); + // let time pass + // following guard is always false as SIFS=1 + // [time] s1=10 & c1=0 & x1>0 & x1 (x1'=min(x1+1,TIME_MAX)); + // ack is sent after SIFS (since SIFS-1=0 add condition that channel is free) + [send1] s1=10 & c1=0 & (x1=SIFS | (x1=SIFS-1 & free)) -> (s1'=10) & (x1'=0); + + // WAIT FOR ACK i.e. c1=1 + // let time pass + [time] s1=10 & c1=1 & x1 (x1'=min(x1+1,TIME_MAX)); + // get acknowledgement so packet sent correctly and move to done + [finish1] s1=10 & c1=1 & (x1=ACK | x1=ACK-1) -> (s1'=12) & (x1'=0) & (bc1'=0); + + // WAIT FOR ACK_TO + // check channel and busy: go into backoff + [] s1=11 & x1=0 & busy -> (s1'=2); + // check channel and free: let time pass + [time] s1=11 & x1=0 & free -> (x1'=min(x1+1,TIME_MAX)); + // let time pass + [time] s1=11 & x1>0 & x1 (x1'=min(x1+1,TIME_MAX)); + // no acknowledgement (go to backoff waiting DIFS first) + [] s1=11 & x1=ACK_TO -> (s1'=3) & (x1'=0); + + // DONE + [time] s1=12 -> (s1'=12); + +endmodule + +// ---------------------------------------------------------------------------- // +// STATION 2 (rename STATION 1) +module +station2=station1[x1=x2, + s1=s2, + s2=s1, + c1=c2, + c2=c1, + slot1=slot2, + backoff1=backoff2, + bc1=bc2, + send1=send2, + finish1=finish2] +endmodule +// ---------------------------------------------------------------------------- // + +label "twoCollisions" = col=2; +label "fourCollisions" = col=4; +label "sixCollisions" = col=6; \ No newline at end of file From 5a4730ae22ddc1ce0e2c5e515792b40da2579399 Mon Sep 17 00:00:00 2001 From: dehnert Date: Wed, 16 Apr 2014 22:41:46 +0200 Subject: [PATCH 2/5] When exporting DDs to the dot format, edges leading to the zero node are now suppressed. Also, nodes in the dot file are now labeled with variable names (+ the number of the bit). Former-commit-id: 410d61d33331d5f9563172016aa8e9376509916c --- .../3rdparty/cudd-2.5.0/src/cudd/cuddExport.c | 19 ++++++++-- src/storage/dd/CuddDd.cpp | 37 ++++++++++++++++++- src/storage/dd/CuddDd.h | 23 ++++++++---- src/storage/dd/CuddDdManager.cpp | 23 ++++++++++++ src/storage/dd/CuddDdManager.h | 7 ++++ test/functional/storage/CuddDdTest.cpp | 4 +- 6 files changed, 99 insertions(+), 14 deletions(-) diff --git a/resources/3rdparty/cudd-2.5.0/src/cudd/cuddExport.c b/resources/3rdparty/cudd-2.5.0/src/cudd/cuddExport.c index 3d8da77ac..2392da36a 100644 --- a/resources/3rdparty/cudd-2.5.0/src/cudd/cuddExport.c +++ b/resources/3rdparty/cudd-2.5.0/src/cudd/cuddExport.c @@ -502,9 +502,11 @@ Cudd_DumpDot( scan = nodelist[j]; while (scan != NULL) { if (st_is_member(visited,(char *) scan)) { - retval = fprintf(fp,"\"%p\";\n", - (void *) ((mask & (ptrint) scan) / sizeof(DdNode))); - if (retval == EOF) goto failure; + if (scan != Cudd_ReadZero(dd)) { + retval = fprintf(fp,"\"%p\";\n", + (void *) ((mask & (ptrint) scan) / sizeof(DdNode))); + if (retval == EOF) goto failure; + } } scan = scan->next; } @@ -541,6 +543,12 @@ Cudd_DumpDot( scan = nodelist[j]; while (scan != NULL) { if (st_is_member(visited,(char *) scan)) { + retval = fprintf(fp, + "\"%p\" [label = \"%s\"];\n", + (void *) ((mask & (ptrint) scan) / + sizeof(DdNode)), inames[dd->invperm[i]]); + if (retval == EOF) goto failure; + if (cuddT(scan) != Cudd_ReadZero(dd)) { retval = fprintf(fp, "\"%p\" -> \"%p\";\n", (void *) ((mask & (ptrint) scan) / @@ -548,6 +556,8 @@ Cudd_DumpDot( (void *) ((mask & (ptrint) cuddT(scan)) / sizeof(DdNode))); if (retval == EOF) goto failure; + } + if (cuddE(scan) != Cudd_ReadZero(dd)) { if (Cudd_IsComplement(cuddE(scan))) { retval = fprintf(fp, "\"%p\" -> \"%p\" [style = dotted];\n", @@ -565,6 +575,7 @@ Cudd_DumpDot( } if (retval == EOF) goto failure; } + } scan = scan->next; } } @@ -578,11 +589,13 @@ Cudd_DumpDot( scan = nodelist[j]; while (scan != NULL) { if (st_is_member(visited,(char *) scan)) { + if (scan != Cudd_ReadZero(dd)) { retval = fprintf(fp,"\"%p\" [label = \"%g\"];\n", (void *) ((mask & (ptrint) scan) / sizeof(DdNode)), cuddV(scan)); if (retval == EOF) goto failure; } + } scan = scan->next; } } diff --git a/src/storage/dd/CuddDd.cpp b/src/storage/dd/CuddDd.cpp index 0e163c5f7..ef204f790 100644 --- a/src/storage/dd/CuddDd.cpp +++ b/src/storage/dd/CuddDd.cpp @@ -55,6 +55,10 @@ namespace storm { return result; } + Dd Dd::operator-() const { + return this->getDdManager()->getZero() - *this; + } + Dd& Dd::operator-=(Dd const& other) { this->cuddAdd -= other.getCuddAdd(); @@ -85,6 +89,12 @@ namespace storm { return result; } + Dd Dd::logicalOr(Dd const& other) const { + std::set metaVariableNames(this->getContainedMetaVariableNames()); + metaVariableNames.insert(other.getContainedMetaVariableNames().begin(), other.getContainedMetaVariableNames().end()); + return Dd(this->getDdManager(), this->getCuddAdd().Or(other.getCuddAdd()), metaVariableNames); + } + Dd& Dd::complement() { this->cuddAdd = ~this->cuddAdd; return *this; @@ -230,7 +240,7 @@ namespace storm { this->cuddAdd = this->cuddAdd.SwapVariables(from, to); } - Dd Dd::multiplyMatrix(Dd const& otherMatrix, std::set const& summationMetaVariableNames) { + Dd Dd::multiplyMatrix(Dd const& otherMatrix, std::set const& summationMetaVariableNames) const { std::vector summationDdVariables; // Create the CUDD summation variables. @@ -358,9 +368,32 @@ namespace storm { if (filename.empty()) { this->getDdManager()->getCuddManager().DumpDot(cuddAddVector); } else { + // Build the name input of the DD. + std::vector ddNames; + std::string ddName("f"); + ddNames.push_back(new char[ddName.size() + 1]); + memcpy(ddNames.back(), ddName.c_str(), 2); + + // Now build the variables names. + std::vector ddVariableNamesAsStrings = this->getDdManager()->getDdVariableNames(); + std::vector ddVariableNames; + for (auto const& element : ddVariableNamesAsStrings) { + ddVariableNames.push_back(new char[element.size() + 1]); + memcpy(ddVariableNames.back(), element.c_str(), element.size() + 1); + } + + // Open the file, dump the DD and close it again. FILE* filePointer = fopen(filename.c_str() , "w"); - this->getDdManager()->getCuddManager().DumpDot(cuddAddVector, nullptr, nullptr, filePointer); + this->getDdManager()->getCuddManager().DumpDot(cuddAddVector, &ddVariableNames[0], &ddNames[0], filePointer); fclose(filePointer); + + // Finally, delete the names. + for (char* element : ddNames) { + delete element; + } + for (char* element : ddVariableNames) { + delete element; + } } } diff --git a/src/storage/dd/CuddDd.h b/src/storage/dd/CuddDd.h index 6da2dc9c3..8ca99614a 100644 --- a/src/storage/dd/CuddDd.h +++ b/src/storage/dd/CuddDd.h @@ -88,6 +88,13 @@ namespace storm { */ Dd operator-(Dd const& other) const; + /*! + * Subtracts the DD from the constant zero function. + * + * @return The resulting function represented as a DD. + */ + Dd operator-() const; + /*! * Subtracts the given DD from the current one and assigns the result to the current DD. * @@ -112,13 +119,6 @@ namespace storm { */ Dd& operator/=(Dd const& other); - /*! - * Subtracts the DD from the constant zero function. - * - * @return The resulting function represented as a DD. - */ - Dd minus() const; - /*! * Retrieves the logical complement of the current DD. The result will map all encodings with a value * unequal to zero to false and all others to true. @@ -126,6 +126,13 @@ namespace storm { * @return The logical complement of the current DD. */ Dd operator~() const; + + /*! + * Performs a logical or of the current and the given DD. + * + * @return The logical or of the operands. + */ + Dd logicalOr(Dd const& other) const; /*! * Logically complements the current DD. The result will map all encodings with a value @@ -232,7 +239,7 @@ namespace storm { * matrix multiplication. * @return A DD representing the result of the matrix-matrix multiplication. */ - Dd multiplyMatrix(Dd const& otherMatrix, std::set const& summationMetaVariableNames); + Dd multiplyMatrix(Dd const& otherMatrix, std::set const& summationMetaVariableNames) const; /*! * Retrieves the number of encodings that are mapped to a non-zero value. diff --git a/src/storage/dd/CuddDdManager.cpp b/src/storage/dd/CuddDdManager.cpp index 9843b5c92..cda474e7f 100644 --- a/src/storage/dd/CuddDdManager.cpp +++ b/src/storage/dd/CuddDdManager.cpp @@ -1,4 +1,5 @@ #include +#include #include #include "src/storage/dd/CuddDdManager.h" @@ -179,5 +180,27 @@ namespace storm { Cudd& DdManager::getCuddManager() { return this->cuddManager; } + + std::vector DdManager::getDdVariableNames() const { + // First, we initialize a list DD variables and their names. + std::vector> variableNamePairs; + for (auto const& nameMetaVariablePair : this->metaVariableMap) { + DdMetaVariable const& metaVariable = nameMetaVariablePair.second; + for (uint_fast64_t variableIndex = 0; variableIndex < metaVariable.getNumberOfDdVariables(); ++variableIndex) { + variableNamePairs.emplace_back(metaVariable.getDdVariables()[variableIndex].getCuddAdd(), metaVariable.getName() + "." + std::to_string(variableIndex)); + } + } + + // Then, we sort this list according to the indices of the ADDs. + std::sort(variableNamePairs.begin(), variableNamePairs.end(), [](std::pair const& a, std::pair const& b) { return a.first.getNode()->index < b.first.getNode()->index; }); + + // Now, we project the sorted vector to its second component. + std::vector result; + for (auto const& element : variableNamePairs) { + result.push_back(element.second); + } + + return result; + } } } \ No newline at end of file diff --git a/src/storage/dd/CuddDdManager.h b/src/storage/dd/CuddDdManager.h index ca3f9c2c3..96daeb34a 100644 --- a/src/storage/dd/CuddDdManager.h +++ b/src/storage/dd/CuddDdManager.h @@ -131,6 +131,13 @@ namespace storm { bool hasMetaVariable(std::string const& metaVariableName) const; private: + /*! + * Retrieves a list of names of the DD variables in the order of their index. + * + * @return A list of DD variable names. + */ + std::vector getDdVariableNames() const; + /*! * Retrieves the underlying CUDD manager. * diff --git a/test/functional/storage/CuddDdTest.cpp b/test/functional/storage/CuddDdTest.cpp index 8a5be849a..01d40164a 100644 --- a/test/functional/storage/CuddDdTest.cpp +++ b/test/functional/storage/CuddDdTest.cpp @@ -150,6 +150,9 @@ TEST(CuddDd, OperatorTest) { dd1 = ~dd3; EXPECT_TRUE(dd1 == manager->getOne()); + + dd3 = dd1.logicalOr(dd2); + EXPECT_TRUE(dd3 == manager->getOne()); dd1 = manager->getIdentity("x"); dd2 = manager->getConstant(5); @@ -253,7 +256,6 @@ TEST(CuddDd, GetSetValueTest) { storm::dd::Dd dd1 = manager->getOne(); ASSERT_NO_THROW(dd1.setValue("x", 4, 2)); EXPECT_EQ(2, dd1.getLeafCount()); - dd1.exportToDot("dd1.dot"); std::map metaVariableToValueMap; metaVariableToValueMap.emplace("x", 1); From 61d4bb956c01437662c1d11fbf72d5cb19dd0c77 Mon Sep 17 00:00:00 2001 From: dehnert Date: Thu, 17 Apr 2014 10:49:01 +0200 Subject: [PATCH 3/5] Added functionality to compare two ADDs up to a given precision. Added logical operator overloads to DD interface. Added tests for all new features. Former-commit-id: 738ad49d62089c5ebf6058abdb182f180d154be4 --- resources/3rdparty/cudd-2.5.0/src/cudd/cudd.h | 1 + .../3rdparty/cudd-2.5.0/src/cudd/cuddSat.c | 65 +++++++++++++++++++ .../3rdparty/cudd-2.5.0/src/obj/cuddObj.cc | 10 +++ .../3rdparty/cudd-2.5.0/src/obj/cuddObj.hh | 4 +- src/storage/dd/CuddDd.cpp | 20 +++++- src/storage/dd/CuddDd.h | 34 +++++++--- src/storage/dd/CuddDdManager.cpp | 4 +- test/functional/storage/CuddDdTest.cpp | 16 +++-- 8 files changed, 136 insertions(+), 18 deletions(-) diff --git a/resources/3rdparty/cudd-2.5.0/src/cudd/cudd.h b/resources/3rdparty/cudd-2.5.0/src/cudd/cudd.h index 5a2c2f952..51d509b35 100644 --- a/resources/3rdparty/cudd-2.5.0/src/cudd/cudd.h +++ b/resources/3rdparty/cudd-2.5.0/src/cudd/cudd.h @@ -964,6 +964,7 @@ extern DdNode * Cudd_Increasing (DdManager *dd, DdNode *f, int i); extern int Cudd_EquivDC (DdManager *dd, DdNode *F, DdNode *G, DdNode *D); extern int Cudd_bddLeqUnless (DdManager *dd, DdNode *f, DdNode *g, DdNode *D); extern int Cudd_EqualSupNorm (DdManager *dd, DdNode *f, DdNode *g, CUDD_VALUE_TYPE tolerance, int pr); +extern int Cudd_EqualSupNormRel (DdManager *dd, DdNode *f, DdNode *g, CUDD_VALUE_TYPE tolerance, int pr); extern DdNode * Cudd_bddMakePrime (DdManager *dd, DdNode *cube, DdNode *f); extern DdNode * Cudd_bddMaximallyExpand(DdManager *dd, DdNode *lb, DdNode *ub, DdNode *f); extern DdNode * Cudd_bddLargestPrimeUnate(DdManager *dd , DdNode *f, DdNode *phaseBdd); diff --git a/resources/3rdparty/cudd-2.5.0/src/cudd/cuddSat.c b/resources/3rdparty/cudd-2.5.0/src/cudd/cuddSat.c index 19dcafff0..869733f32 100644 --- a/resources/3rdparty/cudd-2.5.0/src/cudd/cuddSat.c +++ b/resources/3rdparty/cudd-2.5.0/src/cudd/cuddSat.c @@ -853,6 +853,71 @@ Cudd_EqualSupNorm( } /* end of Cudd_EqualSupNorm */ +/**Function******************************************************************** + + Synopsis [Compares two ADDs for equality within tolerance.] + + Description [Same as Cudd_EqualSupNorm but tests for max _relative_ difference + i.e. (f-g/f)0) { + (void) fprintf(dd->out,"Offending nodes:\n"); + (void) fprintf(dd->out, + "f: address = %p\t value = %40.30f\n", + (void *) f, cuddV(f)); + (void) fprintf(dd->out, + "g: address = %p\t value = %40.30f\n", + (void *) g, cuddV(g)); + } + return(0); + } + } + + /* We only insert the result in the cache if the comparison is + ** successful. Therefore, if we hit we return 1. */ + r = cuddCacheLookup2(dd,(DD_CTFP)Cudd_EqualSupNormRel,f,g); + if (r != NULL) { + return(1); + } + + /* Compute the cofactors and solve the recursive subproblems. */ + topf = cuddI(dd,f->index); + topg = cuddI(dd,g->index); + + if (topf <= topg) {fv = cuddT(f); fvn = cuddE(f);} else {fv = fvn = f;} + if (topg <= topf) {gv = cuddT(g); gvn = cuddE(g);} else {gv = gvn = g;} + + if (!Cudd_EqualSupNormRel(dd,fv,gv,tolerance,pr)) return(0); + if (!Cudd_EqualSupNormRel(dd,fvn,gvn,tolerance,pr)) return(0); + + cuddCacheInsert2(dd,(DD_CTFP)Cudd_EqualSupNormRel,f,g,DD_ONE(dd)); + + return(1); + +} /* end of Cudd_EqualSupNormRel */ /**Function******************************************************************** diff --git a/resources/3rdparty/cudd-2.5.0/src/obj/cuddObj.cc b/resources/3rdparty/cudd-2.5.0/src/obj/cuddObj.cc index c9fcf7b11..2753c0950 100644 --- a/resources/3rdparty/cudd-2.5.0/src/obj/cuddObj.cc +++ b/resources/3rdparty/cudd-2.5.0/src/obj/cuddObj.cc @@ -4747,6 +4747,16 @@ ADD::EqualSupNorm( } // ADD::EqualSupNorm +bool +ADD::EqualSupNormRel( + const ADD& g, + CUDD_VALUE_TYPE tolerance, + int pr) const +{ + DdManager *mgr = checkSameManager(g); + return Cudd_EqualSupNormRel(mgr, node, g.node, tolerance, pr) != 0; + +} // ADD::EqualSupNormRel BDD BDD::MakePrime( diff --git a/resources/3rdparty/cudd-2.5.0/src/obj/cuddObj.hh b/resources/3rdparty/cudd-2.5.0/src/obj/cuddObj.hh index a1a859490..795a7a2ee 100644 --- a/resources/3rdparty/cudd-2.5.0/src/obj/cuddObj.hh +++ b/resources/3rdparty/cudd-2.5.0/src/obj/cuddObj.hh @@ -426,8 +426,8 @@ public: ADD TimesPlus(const ADD& B, std::vector z) const; ADD Triangle(const ADD& g, std::vector z) const; ADD Eval(int * inputs) const; - bool EqualSupNorm(const ADD& g, CUDD_VALUE_TYPE tolerance, int pr) const; - + bool EqualSupNorm(const ADD& g, CUDD_VALUE_TYPE tolerance, int pr = 0) const; + bool EqualSupNormRel(const ADD& g, CUDD_VALUE_TYPE tolerance, int pr = 0) const; }; // ADD diff --git a/src/storage/dd/CuddDd.cpp b/src/storage/dd/CuddDd.cpp index ef204f790..c5fb92bbd 100644 --- a/src/storage/dd/CuddDd.cpp +++ b/src/storage/dd/CuddDd.cpp @@ -83,13 +83,21 @@ namespace storm { return *this; } - Dd Dd::operator~() const { + Dd Dd::operator!() const { Dd result(*this); result.complement(); return result; } + + Dd Dd::operator&&(Dd const& other) const { + std::set metaVariableNames(this->getContainedMetaVariableNames()); + metaVariableNames.insert(other.getContainedMetaVariableNames().begin(), other.getContainedMetaVariableNames().end()); + + // Rewrite a and b to not((not a) or (not b)). + return Dd(this->getDdManager(), ~(~this->getCuddAdd()).Or(~other.getCuddAdd()), metaVariableNames); + } - Dd Dd::logicalOr(Dd const& other) const { + Dd Dd::operator||(Dd const& other) const { std::set metaVariableNames(this->getContainedMetaVariableNames()); metaVariableNames.insert(other.getContainedMetaVariableNames().begin(), other.getContainedMetaVariableNames().end()); return Dd(this->getDdManager(), this->getCuddAdd().Or(other.getCuddAdd()), metaVariableNames); @@ -204,6 +212,14 @@ namespace storm { this->cuddAdd = this->cuddAdd.MaxAbstract(cubeDd.getCuddAdd()); } + bool Dd::equalModuloPrecision(Dd const& other, double precision, bool relative) const { + if (relative) { + return this->getCuddAdd().EqualSupNormRel(other.getCuddAdd(), precision); + } else { + return this->getCuddAdd().EqualSupNorm(other.getCuddAdd(), precision); + } + } + void Dd::swapVariables(std::vector> const& metaVariablePairs) { std::vector from; std::vector to; diff --git a/src/storage/dd/CuddDd.h b/src/storage/dd/CuddDd.h index 8ca99614a..1942f6504 100644 --- a/src/storage/dd/CuddDd.h +++ b/src/storage/dd/CuddDd.h @@ -48,6 +48,20 @@ namespace storm { */ bool operator!=(Dd const& other) const; + /*! + * Performs a logical or of the current and the given DD. + * + * @return The logical or of the operands. + */ + Dd operator||(Dd const& other) const; + + /*! + * Performs a logical and of the current and the given DD. + * + * @return The logical and of the operands. + */ + Dd operator&&(Dd const& other) const; + /*! * Adds the two DDs. * @@ -125,14 +139,7 @@ namespace storm { * * @return The logical complement of the current DD. */ - Dd operator~() const; - - /*! - * Performs a logical or of the current and the given DD. - * - * @return The logical or of the operands. - */ - Dd logicalOr(Dd const& other) const; + Dd operator!() const; /*! * Logically complements the current DD. The result will map all encodings with a value @@ -222,6 +229,17 @@ namespace storm { */ void maxAbstract(std::set const& metaVariableNames); + /*! + * Checks whether the current and the given DD represent the same function modulo some given precision. + * + * @param other The DD with which to compare. + * @param precision An upper bound on the maximal difference between any two function values that is to be + * tolerated. + * @param relative If set to true, not the absolute values have to be within the precision, but the relative + * values. + */ + bool equalModuloPrecision(Dd const& other, double precision, bool relative = true) const; + /*! * Swaps the given pairs of meta variables in the DD. The pairs of meta variables must be guaranteed to have * the same number of underlying DD variables. diff --git a/src/storage/dd/CuddDdManager.cpp b/src/storage/dd/CuddDdManager.cpp index cda474e7f..4352e52b7 100644 --- a/src/storage/dd/CuddDdManager.cpp +++ b/src/storage/dd/CuddDdManager.cpp @@ -45,14 +45,14 @@ namespace storm { if (value & (1ull << (ddVariables.size() - 1))) { result = ddVariables[0]; } else { - result = ~ddVariables[0]; + result = !ddVariables[0]; } for (std::size_t i = 1; i < ddVariables.size(); ++i) { if (value & (1ull << (ddVariables.size() - i - 1))) { result *= ddVariables[i]; } else { - result *= ~ddVariables[i]; + result *= !ddVariables[i]; } } diff --git a/test/functional/storage/CuddDdTest.cpp b/test/functional/storage/CuddDdTest.cpp index 01d40164a..c405006d8 100644 --- a/test/functional/storage/CuddDdTest.cpp +++ b/test/functional/storage/CuddDdTest.cpp @@ -130,9 +130,12 @@ TEST(CuddDd, OperatorTest) { dd3 += manager->getZero(); EXPECT_TRUE(dd3 == manager->getConstant(2)); + dd3 = dd1 && manager->getConstant(3); + EXPECT_TRUE(dd1 == manager->getOne()); + dd3 = dd1 * manager->getConstant(3); EXPECT_TRUE(dd3 == manager->getConstant(3)); - + dd3 *= manager->getConstant(2); EXPECT_TRUE(dd3 == manager->getConstant(6)); @@ -148,10 +151,10 @@ TEST(CuddDd, OperatorTest) { dd3.complement(); EXPECT_TRUE(dd3 == manager->getZero()); - dd1 = ~dd3; + dd1 = !dd3; EXPECT_TRUE(dd1 == manager->getOne()); - dd3 = dd1.logicalOr(dd2); + dd3 = dd1 || dd2; EXPECT_TRUE(dd3 == manager->getOne()); dd1 = manager->getIdentity("x"); @@ -161,7 +164,7 @@ TEST(CuddDd, OperatorTest) { EXPECT_EQ(1, dd3.getNonZeroCount()); storm::dd::Dd dd4 = dd1.notEquals(dd2); - EXPECT_TRUE(dd4 == ~dd3); + EXPECT_TRUE(dd4 == !dd3); dd3 = dd1.less(dd2); EXPECT_EQ(11, dd3.getNonZeroCount()); @@ -174,6 +177,11 @@ TEST(CuddDd, OperatorTest) { dd3 = dd1.greaterOrEqual(dd2); EXPECT_EQ(5, dd3.getNonZeroCount()); + + dd1 = manager->getConstant(0.01); + dd2 = manager->getConstant(0.01 + 1e-6); + EXPECT_TRUE(dd1.equalModuloPrecision(dd2, 1e-6, false)); + EXPECT_FALSE(dd1.equalModuloPrecision(dd2, 1e-6)); } TEST(CuddDd, AbstractionTest) { From 311247ff0cba4b8a38637ce5e8daa5703a9e4422 Mon Sep 17 00:00:00 2001 From: dehnert Date: Thu, 17 Apr 2014 18:30:57 +0200 Subject: [PATCH 4/5] Added support for Xor in expression classes and added parsing functionality for Xor, Implies and Iff. Former-commit-id: 16e023cf26806e7d9c6c7f72073b77bfff975d61 --- src/parser/PrismParser.cpp | 28 +++++++++++++++++-- src/parser/PrismParser.h | 8 ++++-- .../BinaryBooleanFunctionExpression.cpp | 3 ++ .../BinaryBooleanFunctionExpression.h | 2 +- src/storage/expressions/Expression.cpp | 5 ++++ src/storage/expressions/Expression.h | 1 + test/functional/parser/PrismParserTest.cpp | 2 +- test/functional/storage/ExpressionTest.cpp | 6 ++++ 8 files changed, 49 insertions(+), 6 deletions(-) diff --git a/src/parser/PrismParser.cpp b/src/parser/PrismParser.cpp index 6039c2c11..f46b3f691 100644 --- a/src/parser/PrismParser.cpp +++ b/src/parser/PrismParser.cpp @@ -91,10 +91,10 @@ namespace storm { relativeExpression = (plusExpression >> qi::lit(">=") >> plusExpression)[qi::_val = phoenix::bind(&PrismParser::createGreaterOrEqualExpression, phoenix::ref(*this), qi::_1, qi::_2)] | (plusExpression >> qi::lit(">") >> plusExpression)[qi::_val = phoenix::bind(&PrismParser::createGreaterExpression, phoenix::ref(*this), qi::_1, qi::_2)] | (plusExpression >> qi::lit("<=") >> plusExpression)[qi::_val = phoenix::bind(&PrismParser::createLessOrEqualExpression, phoenix::ref(*this), qi::_1, qi::_2)] | (plusExpression >> qi::lit("<") >> plusExpression)[qi::_val = phoenix::bind(&PrismParser::createLessExpression, phoenix::ref(*this), qi::_1, qi::_2)] | (plusExpression >> qi::lit("=") >> plusExpression)[qi::_val = phoenix::bind(&PrismParser::createEqualsExpression, phoenix::ref(*this), qi::_1, qi::_2)] | (plusExpression >> qi::lit("!=") >> plusExpression)[qi::_val = phoenix::bind(&PrismParser::createNotEqualsExpression, phoenix::ref(*this), qi::_1, qi::_2)] | plusExpression[qi::_val = qi::_1]; relativeExpression.name("relative expression"); - andExpression = relativeExpression[qi::_val = qi::_1] >> *(qi::lit("&") >> relativeExpression)[qi::_val = phoenix::bind(&PrismParser::createAndExpression, phoenix::ref(*this), qi::_val, qi::_1)]; + andExpression = relativeExpression[qi::_val = qi::_1] >> *((qi::lit("&")[qi::_a = storm::expressions::BinaryBooleanFunctionExpression::OperatorType::And] | qi::lit("<=>")[qi::_a = storm::expressions::BinaryBooleanFunctionExpression::OperatorType::Iff] | qi::lit("^")[qi::_a = storm::expressions::BinaryBooleanFunctionExpression::OperatorType::Xor]) >> relativeExpression)[phoenix::if_(qi::_a == storm::expressions::BinaryBooleanFunctionExpression::OperatorType::And) [ qi::_val = phoenix::bind(&PrismParser::createAndExpression, phoenix::ref(*this), qi::_val, qi::_1)] .else_ [ phoenix::if_(qi::_a == storm::expressions::BinaryBooleanFunctionExpression::OperatorType::Iff) [ qi::_val = phoenix::bind(&PrismParser::createIffExpression, phoenix::ref(*this), qi::_val, qi::_1) ] .else_ [ qi::_val = phoenix::bind(&PrismParser::createXorExpression, phoenix::ref(*this), qi::_val, qi::_1) ] ] ]; andExpression.name("and expression"); - orExpression = andExpression[qi::_val = qi::_1] >> *(qi::lit("|") >> andExpression)[qi::_val = phoenix::bind(&PrismParser::createOrExpression, phoenix::ref(*this), qi::_val, qi::_1)]; + orExpression = andExpression[qi::_val = qi::_1] >> *((qi::lit("|")[qi::_a = true] | qi::lit("=>")[qi::_a = false]) >> andExpression)[phoenix::if_(qi::_a) [qi::_val = phoenix::bind(&PrismParser::createOrExpression, phoenix::ref(*this), qi::_val, qi::_1)] .else_ [qi::_val = phoenix::bind(&PrismParser::createImpliesExpression, phoenix::ref(*this), qi::_val, qi::_1)] ]; orExpression.name("or expression"); iteExpression = orExpression[qi::_val = qi::_1] >> -(qi::lit("?") > orExpression > qi::lit(":") > orExpression)[qi::_val = phoenix::bind(&PrismParser::createIteExpression, phoenix::ref(*this), qi::_val, qi::_1, qi::_2)]; @@ -271,6 +271,14 @@ namespace storm { } } + storm::expressions::Expression PrismParser::createImpliesExpression(storm::expressions::Expression e1, storm::expressions::Expression e2) const { + if (!this->secondRun) { + return storm::expressions::Expression::createFalse(); + } else { + return e1.implies(e2); + } + } + storm::expressions::Expression PrismParser::createOrExpression(storm::expressions::Expression e1, storm::expressions::Expression e2) const { if (!this->secondRun) { return storm::expressions::Expression::createFalse(); @@ -319,6 +327,22 @@ namespace storm { } } + storm::expressions::Expression PrismParser::createIffExpression(storm::expressions::Expression e1, storm::expressions::Expression e2) const { + if (!this->secondRun) { + return storm::expressions::Expression::createFalse(); + } else { + return e1.iff(e2); + } + } + + storm::expressions::Expression PrismParser::createXorExpression(storm::expressions::Expression e1, storm::expressions::Expression e2) const { + if (!this->secondRun) { + return storm::expressions::Expression::createFalse(); + } else { + return e1 ^ e2; + } + } + storm::expressions::Expression PrismParser::createEqualsExpression(storm::expressions::Expression e1, storm::expressions::Expression e2) const { if (!this->secondRun) { return storm::expressions::Expression::createFalse(); diff --git a/src/parser/PrismParser.h b/src/parser/PrismParser.h index 3f8f17b65..de3effa32 100644 --- a/src/parser/PrismParser.h +++ b/src/parser/PrismParser.h @@ -25,6 +25,7 @@ typedef BOOST_TYPEOF(qi::lit("//") >> *(qi::char_ - qi::eol) >> qi::eol | boost: #include "src/storage/prism/Program.h" #include "src/storage/expressions/Expression.h" +#include "src/storage/expressions/Expressions.h" #include "src/exceptions/ExceptionMacros.h" namespace storm { @@ -244,8 +245,8 @@ namespace storm { // Rules for parsing a composed expression. qi::rule expression; qi::rule iteExpression; - qi::rule orExpression; - qi::rule andExpression; + qi::rule, Skipper> orExpression; + qi::rule, Skipper> andExpression; qi::rule relativeExpression; qi::rule, Skipper> plusExpression; qi::rule, Skipper> multiplicationExpression; @@ -269,12 +270,15 @@ namespace storm { bool addInitialStatesExpression(storm::expressions::Expression initialStatesExpression, GlobalProgramInformation& globalProgramInformation); storm::expressions::Expression createIteExpression(storm::expressions::Expression e1, storm::expressions::Expression e2, storm::expressions::Expression e3) const; + storm::expressions::Expression createImpliesExpression(storm::expressions::Expression e1, storm::expressions::Expression e2) const; storm::expressions::Expression createOrExpression(storm::expressions::Expression e1, storm::expressions::Expression e2) const; storm::expressions::Expression createAndExpression(storm::expressions::Expression e1, storm::expressions::Expression e2) const; storm::expressions::Expression createGreaterExpression(storm::expressions::Expression e1, storm::expressions::Expression e2) const; storm::expressions::Expression createGreaterOrEqualExpression(storm::expressions::Expression e1, storm::expressions::Expression e2) const; storm::expressions::Expression createLessExpression(storm::expressions::Expression e1, storm::expressions::Expression e2) const; storm::expressions::Expression createLessOrEqualExpression(storm::expressions::Expression e1, storm::expressions::Expression e2) const; + storm::expressions::Expression createIffExpression(storm::expressions::Expression e1, storm::expressions::Expression e2) const; + storm::expressions::Expression createXorExpression(storm::expressions::Expression e1, storm::expressions::Expression e2) const; storm::expressions::Expression createEqualsExpression(storm::expressions::Expression e1, storm::expressions::Expression e2) const; storm::expressions::Expression createNotEqualsExpression(storm::expressions::Expression e1, storm::expressions::Expression e2) const; storm::expressions::Expression createPlusExpression(storm::expressions::Expression e1, storm::expressions::Expression e2) const; diff --git a/src/storage/expressions/BinaryBooleanFunctionExpression.cpp b/src/storage/expressions/BinaryBooleanFunctionExpression.cpp index 9f5e5edeb..d5d6694ab 100644 --- a/src/storage/expressions/BinaryBooleanFunctionExpression.cpp +++ b/src/storage/expressions/BinaryBooleanFunctionExpression.cpp @@ -23,6 +23,7 @@ namespace storm { switch (this->getOperatorType()) { case OperatorType::And: result = firstOperandEvaluation && secondOperandEvaluation; break; case OperatorType::Or: result = firstOperandEvaluation || secondOperandEvaluation; break; + case OperatorType::Xor: result = firstOperandEvaluation ^ secondOperandEvaluation; break; case OperatorType::Implies: result = !firstOperandEvaluation || secondOperandEvaluation; break; case OperatorType::Iff: result = (firstOperandEvaluation && secondOperandEvaluation) || (!firstOperandEvaluation && !secondOperandEvaluation); break; } @@ -55,6 +56,7 @@ namespace storm { return firstOperandSimplified; } break; + case OperatorType::Xor: break; case OperatorType::Implies: if (firstOperandSimplified->isTrue()) { return secondOperandSimplified; } else if (firstOperandSimplified->isFalse()) { @@ -88,6 +90,7 @@ namespace storm { switch (this->getOperatorType()) { case OperatorType::And: stream << " & "; break; case OperatorType::Or: stream << " | "; break; + case OperatorType::Xor: stream << " ^ "; break; case OperatorType::Implies: stream << " => "; break; case OperatorType::Iff: stream << " <=> "; break; } diff --git a/src/storage/expressions/BinaryBooleanFunctionExpression.h b/src/storage/expressions/BinaryBooleanFunctionExpression.h index 7a05a1ab5..8b1bb7437 100644 --- a/src/storage/expressions/BinaryBooleanFunctionExpression.h +++ b/src/storage/expressions/BinaryBooleanFunctionExpression.h @@ -11,7 +11,7 @@ namespace storm { /*! * An enum type specifying the different operators applicable. */ - enum class OperatorType {And, Or, Implies, Iff}; + enum class OperatorType {And, Or, Xor, Implies, Iff}; /*! * Creates a binary boolean function expression with the given return type, operands and operator. diff --git a/src/storage/expressions/Expression.cpp b/src/storage/expressions/Expression.cpp index 7eb94966b..5b5a2bfb6 100644 --- a/src/storage/expressions/Expression.cpp +++ b/src/storage/expressions/Expression.cpp @@ -166,6 +166,11 @@ namespace storm { return Expression(std::shared_ptr(new BinaryNumericalFunctionExpression(this->getReturnType() == ExpressionReturnType::Int && other.getReturnType() == ExpressionReturnType::Int ? ExpressionReturnType::Int : ExpressionReturnType::Double, this->getBaseExpressionPointer(), other.getBaseExpressionPointer(), BinaryNumericalFunctionExpression::OperatorType::Divide))); } + Expression Expression::operator^(Expression const& other) const { + LOG_THROW(this->hasBooleanReturnType() && other.hasBooleanReturnType(), storm::exceptions::InvalidTypeException, "Operator '^' requires boolean operands."); + return Expression(std::shared_ptr(new BinaryBooleanFunctionExpression(ExpressionReturnType::Bool, this->getBaseExpressionPointer(), other.getBaseExpressionPointer(), BinaryBooleanFunctionExpression::OperatorType::Xor))); + } + Expression Expression::operator&&(Expression const& other) const { LOG_THROW(this->hasBooleanReturnType() && other.hasBooleanReturnType(), storm::exceptions::InvalidTypeException, "Operator '&&' requires boolean operands."); return Expression(std::shared_ptr(new BinaryBooleanFunctionExpression(ExpressionReturnType::Bool, this->getBaseExpressionPointer(), other.getBaseExpressionPointer(), BinaryBooleanFunctionExpression::OperatorType::And))); diff --git a/src/storage/expressions/Expression.h b/src/storage/expressions/Expression.h index ea7d99572..d751dfbb9 100644 --- a/src/storage/expressions/Expression.h +++ b/src/storage/expressions/Expression.h @@ -47,6 +47,7 @@ namespace storm { Expression operator-() const; Expression operator*(Expression const& other) const; Expression operator/(Expression const& other) const; + Expression operator^(Expression const& other) const; Expression operator&&(Expression const& other) const; Expression operator||(Expression const& other) const; Expression operator!() const; diff --git a/test/functional/parser/PrismParserTest.cpp b/test/functional/parser/PrismParserTest.cpp index 739d9ca5b..381ca3e1b 100644 --- a/test/functional/parser/PrismParserTest.cpp +++ b/test/functional/parser/PrismParserTest.cpp @@ -47,7 +47,7 @@ TEST(PrismParser, SimpleFullTest) { R"(dtmc module mod1 b : bool; - [a] true -> 1: (b'=true); + [a] true -> 1: (b'=true ^ false <=> b => false); endmodule)"; storm::prism::Program result; diff --git a/test/functional/storage/ExpressionTest.cpp b/test/functional/storage/ExpressionTest.cpp index 0c19c5bfb..6ce9f50c5 100644 --- a/test/functional/storage/ExpressionTest.cpp +++ b/test/functional/storage/ExpressionTest.cpp @@ -264,6 +264,12 @@ TEST(Expression, OperatorTest) { ASSERT_NO_THROW(tempExpression = boolVarExpression.iff(boolConstExpression)); EXPECT_TRUE(tempExpression.getReturnType() == storm::expressions::ExpressionReturnType::Bool); + ASSERT_THROW(tempExpression = trueExpression ^ piExpression, storm::exceptions::InvalidTypeException); + ASSERT_NO_THROW(tempExpression = trueExpression ^ falseExpression); + EXPECT_TRUE(tempExpression.getReturnType() == storm::expressions::ExpressionReturnType::Bool); + ASSERT_NO_THROW(tempExpression = boolVarExpression ^ boolConstExpression); + EXPECT_TRUE(tempExpression.getReturnType() == storm::expressions::ExpressionReturnType::Bool); + ASSERT_THROW(tempExpression = trueExpression.floor(), storm::exceptions::InvalidTypeException); ASSERT_NO_THROW(tempExpression = threeExpression.floor()); EXPECT_TRUE(tempExpression.getReturnType() == storm::expressions::ExpressionReturnType::Int); From d57a0c9901ca75d287ac68d3662badc777ae5c9f Mon Sep 17 00:00:00 2001 From: dehnert Date: Thu, 17 Apr 2014 18:41:36 +0200 Subject: [PATCH 5/5] Replaced memcpy by std::copy. Former-commit-id: ef31cf99772064aa660ee1acfc7ab05037b8087a --- src/storage/dd/CuddDd.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/storage/dd/CuddDd.cpp b/src/storage/dd/CuddDd.cpp index c5fb92bbd..7ea5ab260 100644 --- a/src/storage/dd/CuddDd.cpp +++ b/src/storage/dd/CuddDd.cpp @@ -388,14 +388,14 @@ namespace storm { std::vector ddNames; std::string ddName("f"); ddNames.push_back(new char[ddName.size() + 1]); - memcpy(ddNames.back(), ddName.c_str(), 2); + std::copy(ddName.c_str(), ddName.c_str() + 2, ddNames.back()); // Now build the variables names. std::vector ddVariableNamesAsStrings = this->getDdManager()->getDdVariableNames(); std::vector ddVariableNames; for (auto const& element : ddVariableNamesAsStrings) { ddVariableNames.push_back(new char[element.size() + 1]); - memcpy(ddVariableNames.back(), element.c_str(), element.size() + 1); + std::copy(element.c_str(), element.c_str() + element.size() + 1, ddVariableNames.back()); } // Open the file, dump the DD and close it again.