From b85ca822fc71086934c08b987b26cf17badafe81 Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Mon, 6 Apr 2020 14:23:39 +0100 Subject: [PATCH] POPTA regression tests. --- .../verify/poptas/example1.prism | 38 ++++++ .../verify/poptas/example1.prism.props | 2 + .../verify/poptas/example2.prism | 41 +++++++ .../verify/poptas/example2.prism.props | 2 + .../verify/poptas/pump_popta.prism.props.args | 1 + prism/tests/poptas/pump_popta.prism | 116 ++++++++++++++++++ prism/tests/poptas/pump_popta.prism.args | 1 + prism/tests/poptas/pump_popta.prism.props | 13 ++ prism/tests/poptas/pump_popta_deadline.prism | 76 ++++++++++++ .../poptas/pump_popta_deadline.prism.args | 1 + .../poptas/pump_popta_deadline.prism.props | 9 ++ 11 files changed, 300 insertions(+) create mode 100644 prism-tests/functionality/verify/poptas/example1.prism create mode 100644 prism-tests/functionality/verify/poptas/example1.prism.props create mode 100644 prism-tests/functionality/verify/poptas/example2.prism create mode 100644 prism-tests/functionality/verify/poptas/example2.prism.props create mode 100644 prism-tests/functionality/verify/poptas/pump_popta.prism.props.args create mode 100644 prism/tests/poptas/pump_popta.prism create mode 100644 prism/tests/poptas/pump_popta.prism.args create mode 100644 prism/tests/poptas/pump_popta.prism.props create mode 100644 prism/tests/poptas/pump_popta_deadline.prism create mode 100644 prism/tests/poptas/pump_popta_deadline.prism.args create mode 100644 prism/tests/poptas/pump_popta_deadline.prism.props diff --git a/prism-tests/functionality/verify/poptas/example1.prism b/prism-tests/functionality/verify/poptas/example1.prism new file mode 100644 index 00000000..679aa17f --- /dev/null +++ b/prism-tests/functionality/verify/poptas/example1.prism @@ -0,0 +1,38 @@ +// Example 1 from +// "Verification and Control of Partially Observable Probabilistic Real-Time Systems" +// Norman/Parker/Zou, FORMATS 2015 +// Or Example 3 from +// "Verification and Control of Partially Observable Probabilistic Systems" +// Norman/Parker/Zou, Real-Time Systems, 53(3), 2017 + +popta + +observables + x, y, o +endobservables + +module M + + l : [0..5] init 0; + o : [0..4] init 0; // 0, 1&2, 3, 4, 5 + x : clock; + y : clock; + + invariant + (l=0 => x<=1) & + (l=1 => true) & + (l=2 => true) & + (l=3 => true) & + (l=4 => true) & + (l=5 => true) + endinvariant + + [a0] l=0 & x>=1 -> 1/2 : (l'=1)&(o'=1) + 1/2 : (l'=2)&(o'=1); + [a] l=1 -> (l'=3)&(o'=2); + [a] l=2 -> (l'=4)&(o'=3)&(x'=0); + [b] l=3 & y=1 -> (l'=5)&(o'=4); + [b] l=4 & y=2 & x=0 -> (l'=5)&(o'=4); + +endmodule + +label "goal" = o=4; diff --git a/prism-tests/functionality/verify/poptas/example1.prism.props b/prism-tests/functionality/verify/poptas/example1.prism.props new file mode 100644 index 00000000..05d73cd6 --- /dev/null +++ b/prism-tests/functionality/verify/poptas/example1.prism.props @@ -0,0 +1,2 @@ +// RESULT: 0.5 +Pmax=? [ F "goal" ] diff --git a/prism-tests/functionality/verify/poptas/example2.prism b/prism-tests/functionality/verify/poptas/example2.prism new file mode 100644 index 00000000..ecfe0c23 --- /dev/null +++ b/prism-tests/functionality/verify/poptas/example2.prism @@ -0,0 +1,41 @@ +// Example 2 from +// "Verification and Control of Partially Observable Probabilistic Real-Time Systems" +// Norman/Parker/Zou, FORMATS 2015 +// Or Example 4 from +// "Verification and Control of Partially Observable Probabilistic Systems" +// Norman/Parker/Zou, Real-Time Systems, 53(3), 2017 + +popta + +observables x, o endobservables + +module M + + x : clock; + l : [0..3] init 0; + o : [0..2] init 0; // 0, 1&2, 3 + + invariant + (l=0 => x<=1) & + (l=1 => x<=2) & + (l=2 => x<=2) & + (l=3 => true) + endinvariant + + [a0] l=0 & x<=1 -> 1/2 : (l'=1)&(o'=1) + 1/2 : (l'=2)&(o'=1)&(x'=0); + + [a1] l=1 & x<=2 -> (l'=3)&(o'=2); + [a2] l=1 & x<=2 -> (l'=3)&(o'=2); + + [a1] l=2 & x<=2 -> (l'=3)&(o'=2); + [a2] l=2 & x<=2 -> (l'=3)&(o'=2); + +endmodule + +label "goal" = o=2; + +rewards + [a2] l=1 : 1; + [a1] l=2 : 1; + l=0 : 1; +endrewards diff --git a/prism-tests/functionality/verify/poptas/example2.prism.props b/prism-tests/functionality/verify/poptas/example2.prism.props new file mode 100644 index 00000000..42dbf8dd --- /dev/null +++ b/prism-tests/functionality/verify/poptas/example2.prism.props @@ -0,0 +1,2 @@ +// RESULT: 0.5 +Rmin=? [ F "goal" ] diff --git a/prism-tests/functionality/verify/poptas/pump_popta.prism.props.args b/prism-tests/functionality/verify/poptas/pump_popta.prism.props.args new file mode 100644 index 00000000..02f576f2 --- /dev/null +++ b/prism-tests/functionality/verify/poptas/pump_popta.prism.props.args @@ -0,0 +1 @@ +-const D=25 diff --git a/prism/tests/poptas/pump_popta.prism b/prism/tests/poptas/pump_popta.prism new file mode 100644 index 00000000..c9e05b22 --- /dev/null +++ b/prism/tests/poptas/pump_popta.prism @@ -0,0 +1,116 @@ +// POPTA model of NRL pump +// dxp/gxn 28/08/14 + +// high is trying to send either 0 or 1 to low through a number of messages +// we assume high uses delays h0 and h1 to transmit either 0 or 1 +// also assume high always sends with this delay +// so this is the average recorded by the pump +// low sends repeated messages to try and figure out what high is transmitting +// based on the time until it receives acks for the messages from the pump + +// model is a POPTA +popta + +// can see the state of the pump and its local variables and all clocks +observables + p, messages, l, m, guess, correct, x, y +endobservables + +// delays for high sending 0 and 1 (both need to be >1) +const int h0; +const int h1; + +// number of messages low can send before guessing +const int N; + +// timeout for low (means a nack and low resends message) +const int Tout = 10; + +// we do not need to model high getting messages and sending acks +// as we assume the delay is fixed (depending on what it is trying to send to low) +// and only the average time for high to respond influence the time the pump +// delays before sending acks to low + +module high + + bit : [-1..1] init -1; // bit high is trying transmit + + // randomly choose bit it is trying to send to low + [] bit=-1 -> 1/2 : (bit'=0) + 1/2 : (bit'=1); + +endmodule + +module pump + + p : [0..2] init 0; // local state + // 0 get message from low + // 1 delaying before ack + // 2 sending ack + + y : clock; // the pump's clock + + invariant + (p=0 => true) & + (p=1 => y<=1) & + (p=2 => y<=0) + endinvariant + + // get message from low (need high to choose first) + [mess_l] p=0 & bit>=0 -> (p'=1) & (y'=0); + + // random delay before ack based on average from high + // this would be letting time pass PTA model + [] p=1 & bit=0 & y=1 -> 1/h0 : (p'=2) & (y'=0) + (1 - 1/h0) : (p'=1) & (y'=0); // av. response high equals h0 + [] p=1 & bit=1 & y=1 -> 1/h1 : (p'=2) & (y'=0) + (1 - 1/h1) : (p'=1) & (y'=0); // av. response high equals h1 + + // receives a new message from low + // this means low timed out (nack) + // so delete old message and start sending an ack for the new message + [mess_l] p>0 -> (p'=0) & (y'=0); + + // send ack (immediately) + [ack_l] p=2 -> (p'=0); + +endmodule + +module low + + l : [0..3] init 0; // local state of low + // 0 send message + // 1 waiting for ack + // 2 guess/check value + // 3 done + + m : [0..N] init 1; // messages low can send before guessing + guess : [-1..1] init -1; // guess low makes + correct : [0..1] init 0; // is it correct or not + + x : clock; // low's clock + + invariant + (l=0 => x<=0) & + (l=1 => x<=Tout) & + (l=2 => x<=0) & + (l=3 => true) + endinvariant + + [mess_l] l=0 -> (l'=1) & (x'=0); // low immediately sends message and waits for an ack + [ack_l] l=1 & m (l'=0) & (m'=m+1) & (x'=0); // ack (more to send) + [ack_l] l=1 & m=N & x<=Tout -> (l'=2) & (x'=0); // ack (time to guess) + [nack_l] l=1 & x=Tout -> (l'=0) & (x'=0); // timeout (nack) + + // when finished sending immediately guess value high was trying to send + [] l=2 & guess=-1 & x=0 -> (guess'=0); + [] l=2 & guess=-1 & x=0 -> (guess'=1); + // and then immediately check if it is correct + [] l=2 & guess>=0 & guess=bit & x=0 -> (l'=3) & (correct'=1); + [] l=2 & guess>=0 & guess!=bit & x=0 -> (l'=3); + +endmodule + +// reward structures +// time +rewards "time" + true : 1; +endrewards + diff --git a/prism/tests/poptas/pump_popta.prism.args b/prism/tests/poptas/pump_popta.prism.args new file mode 100644 index 00000000..d6954984 --- /dev/null +++ b/prism/tests/poptas/pump_popta.prism.args @@ -0,0 +1 @@ +-const h0=2,h1=16,N=3 diff --git a/prism/tests/poptas/pump_popta.prism.props b/prism/tests/poptas/pump_popta.prism.props new file mode 100644 index 00000000..25aaeae1 --- /dev/null +++ b/prism/tests/poptas/pump_popta.prism.props @@ -0,0 +1,13 @@ +const int D; + +// RESULT (h0=2,h1=16,N=3): [0.020656523490556817,0.026807197082692098] (grid resolution 16) +Pmin=? [ F correct=1 ] + +// RESULT (h0=2,h1=16,N=3): [0.9731909334062754,0.9793309413525038] (grid resolution 16) +Pmax=? [ F correct=1 ] + +// RESULT (h0=2,h1=16,N=3,D=25): [0.022890048319850906,0.02541857957662759] (grid resolution 32) +Pmin=? [ F<=D correct=1 ] + +// RESULT (h0=2,h1=16,N=3,D=25): [0.5274229036098491,0.5301895230846264] (grid resolution 32) +Pmax=? [ F<=D correct=1 ] diff --git a/prism/tests/poptas/pump_popta_deadline.prism b/prism/tests/poptas/pump_popta_deadline.prism new file mode 100644 index 00000000..bf9d90dd --- /dev/null +++ b/prism/tests/poptas/pump_popta_deadline.prism @@ -0,0 +1,76 @@ +pomdp + +// can see the state of the pump and its local variables and all clocks +observables + p, messages, l, m, guess, correct, x, y, t +endobservables + +label "invariants" = (p=0=>true)&(p=1=>y<=1)&(p=2=>y<=0)&(l=0=>x<=0)&(l=1=>x<=Tout)&(l=2=>x<=0)&(l=3=>true); + +const int h0; +const int h1; +const int N; +const int Tout = 10; + +const int D; // deadline +module timer + + // global time + t : [0..D+1]; + + // time increases + [time] (t (t'=min(t+1,D+1)); + // loop when deadline has passed + [] (t>D) -> (t'=t); + +endmodule + + +module high + + bit : [-1..1] init -1; + + [] bit=-1 -> 1/2 : (bit'=0) + 1/2 : (bit'=1); + [time] true -> 1.0 : true; + +endmodule + +module pump + + p : [0..2] init 0; + y : [0..2]; + + [mess_l] p=0&bit>=0 -> (p'=1) & (y'=0); + [] p=1&bit=0&y=1 -> 1/h0 : (p'=2) & (y'=0) + (1-1/h0) : (p'=1) & (y'=0); + [] p=1&bit=1&y=1 -> 1/h1 : (p'=2) & (y'=0) + (1-1/h1) : (p'=1) & (y'=0); + [mess_l] p>0 -> (p'=0) & (y'=0); + [ack_l] p=2 -> (p'=0); + [time] (p=0=>true)&(p=1=>y+1<=1)&(p=2=>y+1<=0) -> 1.0 : (y'=min(y+1, 2)); + +endmodule + +module low + + l : [0..3] init 0; + m : [0..N] init 1; + guess : [-1..1] init -1; + correct : [0..1] init 0; + x : [0..11]; + + [mess_l] l=0 -> (l'=1) & (x'=0); + [ack_l] l=1&m (l'=0) & (m'=m+1) & (x'=0); + [ack_l] l=1&m=N&x<=Tout -> (l'=2) & (x'=0); + [nack_l] l=1&x=Tout -> (l'=0) & (x'=0); + [] l=2&guess=-1&x=0 -> (guess'=0); + [] l=2&guess=-1&x=0 -> (guess'=1); + [] l=2&guess>=0&guess=bit&x=0&t<=D -> (l'=3) & (correct'=1); + [] l=2&guess>=0&guess!=bit&x=0&t<=D -> (l'=3); + [time] (l=0=>x+1<=0)&(l=1=>x+1<=Tout)&(l=2=>x+1<=0)&(l=3=>true) -> 1.0 : (x'=min(x+1, 11)); + +endmodule + +rewards "time" + + [time] true : 1; + +endrewards diff --git a/prism/tests/poptas/pump_popta_deadline.prism.args b/prism/tests/poptas/pump_popta_deadline.prism.args new file mode 100644 index 00000000..03a366ce --- /dev/null +++ b/prism/tests/poptas/pump_popta_deadline.prism.args @@ -0,0 +1 @@ +-const h0=2,h1=8,N=4,D=25 diff --git a/prism/tests/poptas/pump_popta_deadline.prism.props b/prism/tests/poptas/pump_popta_deadline.prism.props new file mode 100644 index 00000000..8532c132 --- /dev/null +++ b/prism/tests/poptas/pump_popta_deadline.prism.props @@ -0,0 +1,9 @@ +// RESULT (h0=2,h1=8,N=4,D=25): [0.04801036199374414,0.054256665101135595] (grid resolution 16) +Pmin=? [ F correct=1 ] + +// RESULT (h0=2,h1=8,N=4,D=25): [0.5777239051355592,0.5845244516132015] (grid resolution 16) +Pmax=? [ F correct=1 ] + +//Rmin=? [ F l=2 ] + +//Rmin=? [ F l=2 ]