diff --git a/src/parser/SpiritErrorHandler.h b/src/parser/SpiritErrorHandler.h index cd2a35b06..949ad9b12 100644 --- a/src/parser/SpiritErrorHandler.h +++ b/src/parser/SpiritErrorHandler.h @@ -16,7 +16,7 @@ namespace storm { qi::error_handler_result operator()(T1 b, T2 e, T3 where, T4 const& what) const { auto lineStart = boost::spirit::get_line_start(b, where); auto lineEnd = std::find(where, e, '\n'); - std::string line(++lineStart, lineEnd); + std::string line(lineStart, lineEnd); std::stringstream stream; stream << "Parsing error at " << get_line(where) << ":" << boost::spirit::get_column(lineStart, where) << ": " << " expecting " << what << ", here:" << std::endl; diff --git a/test/performance/builder/leader5.nm b/test/performance/builder/leader5.nm index c48a255bb..26316affa 100644 --- a/test/performance/builder/leader5.nm +++ b/test/performance/builder/leader5.nm @@ -1,4 +1,3 @@ -<<<<<<< HEAD // asynchronous leader election // 4 processes // gxn/dxp 29/01/01 @@ -96,104 +95,3 @@ endrewards //---------------------------------------------------------------------------------------------------------------------------- formula leaders = (s1=4?1:0)+(s2=4?1:0)+(s3=4?1:0)+(s4=4?1:0)+(s5=4?1:0); label "elected" = s1=4|s2=4|s3=4|s4=4|s5=4; - -======= -// asynchronous leader election -// 4 processes -// gxn/dxp 29/01/01 - -mdp - -const int N= 5; // number of processes - -//---------------------------------------------------------------------------------------------------------------------------- -module process1 - - // COUNTER - c1 : [0..5-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 - [p51] (s1=1) & (receive1=0) & !( (p1=0) & (p5=1) ) -> (s1'=2) & (receive1'=1); - // become inactive - [p51] (s1=1) & (receive1=0) & (p1=0) & (p5=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) - [c51] (s1=2) & (receive1=1) & (sent1<2) -> (receive1'=2); - // receive counter and sent counter - // only active process (decide) - [c51] (s1=2) & (receive1=1) & (sent1=2) & (c5=N-1) -> (s1'=4) & (p1'=0) & (c1'=0) & (sent1'=0) & (receive1'=0); - // other active process (pick again) - [c51] (s1=2) & (receive1=1) & (sent1=2) & (c5 (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 - [p51] (s1=3) & (receive1=0) -> (p1'=p5) & (receive1'=1); - // receive counter - [c51] (s1=3) & (receive1=1) & (c5 (c1'=c5+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,p51=p12,c12=c23,c51=c12,p5=p1,c5=c1] endmodule -module process3=process1[s1=s3,p1=p3,c1=c3,sent1=sent3,receive1=receive3,p12=p34,p51=p23,c12=c34,c51=c23,p5=p2,c5=c2] endmodule -module process4=process1[s1=s4,p1=p4,c1=c4,sent1=sent4,receive1=receive4,p12=p45,p51=p34,c12=c45,c51=c34,p5=p3,c5=c3] endmodule -module process5=process1[s1=s5,p1=p5,c1=c5,sent1=sent5,receive1=receive5,p12=p51,p51=p45,c12=c51,c51=c45,p5=p4,c5=c4] endmodule - -//---------------------------------------------------------------------------------------------------------------------------- - -// reward - expected number of rounds (equals the number of times a process receives a counter) -rewards "rounds" - [c12] true : 1; -endrewards - -//---------------------------------------------------------------------------------------------------------------------------- -formula leaders = (s1=4?1:0)+(s2=4?1:0)+(s3=4?1:0)+(s4=4?1:0)+(s5=4?1:0); -label "elected" = s1=4|s2=4|s3=4|s4=4|s5=4; - ->>>>>>> 90d2b218a044edca8062084ee89d171695149c1e diff --git a/test/performance/builder/leader5_8.pm b/test/performance/builder/leader5_8.pm index e6cfc2106..eb7dd9fd7 100644 --- a/test/performance/builder/leader5_8.pm +++ b/test/performance/builder/leader5_8.pm @@ -1,4 +1,3 @@ -<<<<<<< HEAD // synchronous leader election protocol (itai & Rodeh) // dxp/gxn 25/01/01 @@ -88,96 +87,3 @@ endrewards // labels label "elected" = s1=3&s2=3&s3=3&s4=3&s5=3; - -======= -// synchronous leader election protocol (itai & Rodeh) -// dxp/gxn 25/01/01 - -dtmc - -// CONSTANTS -const int N = 5; // number of processes -const int K = 8; // 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 (c'=c+1); - // finished reading - [read] c=N-1 -> (c'=c); - //decide - [done] u1|u2|u3|u4|u5 -> (c'=c); - // pick again reset counter - [retry] !(u1|u2|u3|u4|u5) -> (c'=1); - // loop (when finished to avoid deadlocks) - [loop] s1=3 -> (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) - + 1/K : (s1'=1) & (p1'=5) & (v1'=5) & (u1'=true) - + 1/K : (s1'=1) & (p1'=6) & (v1'=6) & (u1'=true) - + 1/K : (s1'=1) & (p1'=7) & (v1'=7) & (u1'=true); - // read - [read] s1=1 & u1 & c (u1'=(p1!=v2)) & (v1'=v2); - [read] s1=1 & !u1 & c (u1'=false) & (v1'=v2) & (p1'=0); - // read and move to decide - [read] s1=1 & u1 & c=N-1 -> (s1'=2) & (u1'=(p1!=v2)) & (v1'=0) & (p1'=0); - [read] s1=1 & !u1 & c=N-1 -> (s1'=2) & (u1'=false) & (v1'=0); - // deciding - // done - [done] s1=2 -> (s1'=3) & (u1'=false) & (v1'=0) & (p1'=0); - //retry - [retry] s1=2 -> (s1'=0) & (u1'=false) & (v1'=0) & (p1'=0); - // loop (when finished to avoid deadlocks) - [loop] s1=3 -> (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=v4 ] endmodule -module process4 = process1 [ s1=s4,p1=p4,v1=v4,u1=u4,v2=v5 ] endmodule -module process5 = process1 [ s1=s5,p1=p5,v1=v5,u1=u5,v2=v1 ] endmodule - -// expected number of rounds -rewards "num_rounds" - [pick] true : 1; -endrewards - -// labels -label "elected" = s1=3&s2=3&s3=3&s4=3&s5=3; - ->>>>>>> 90d2b218a044edca8062084ee89d171695149c1e