s14h
/
prism-accumulation
1
0
Fork 0
Code Releases Activity
Browse Source

expected properties added to firewire abstion version 

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@846 bbc10eb1-c90d-0410-af57-cb519fbb1720
master
Gethin Norman 17 years ago
parent
0c17fc2e31
commit
7b195d996d
3 changed files with 151 additions and 123 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 10
      prism-examples/firewire/abst/auto
  2. 69
      prism-examples/firewire/abst/deadline.nm
  3. 85
      prism-examples/firewire/abst/firewire.nm

10
prism-examples/firewire/abst/auto
View File

@ -1,9 +1,15 @@
#!/bin/csh
# liveness
prism firewire.nm liveness.pctl -m
prism firewire.nm liveness.pctl -const delay=36,fast=0.5 -m
# maximum expected time
prism firewire.nm expected.pctl -const delay=36,fast=0.2:0.1:0.8 -m -prop 1
# maximum expected time
prism firewire.nm expected.pctl -const delay=36,fast=0.2:0.1:0.8 -m -prop 1
# deadline properties
foreach deadline (200 300 400 500 600) # 800 1000)
prism deadline.nm deadline.pctl -const deadline=$deadline -m
prism deadline.nm deadline.pctl -const deadline=$deadline,delay=36,fast=0.5 -m
end

69
prism-examples/firewire/abst/deadline.nm
View File

@ -1,15 +1,19 @@
// integer semantics version of abstract firewire protocol
// with clock for deadline properties
// gxn 23/05/2001
mdp
//deadline
// deadline
const int deadline;
// largest constant the deadline clock is compared to
const int ky = deadline;
// wire delay (based on max length of wire)
const int delay;
// probability of choosing fast
const double fast;
const double slow = 1-fast;
// largest constant the clock of the system is compared to
// maximal constant
const int kx = 167;
module abstract_firewire
@ -17,55 +21,56 @@ module abstract_firewire
// deadline clock
y : [0..ky+1];
// clock of the system
// model clock
x : [0..kx+1];
// local state
s : [0..10];
// 0 - start_start
// 1 - fast_start
// 2 - start_fast
// 3 - start_slow
// 4 - slow_start
// 5 - fast_fast
// 6 - fast_slow
// 7 - slow_fast
// 8 - slow_slow
// 9 - done
// 10 - deadline exceeded
// 0 -start_start
// 1 -fast_start
// 2 -start_fast
// 3 -start_slow
// 4 -slow_start
// 5 -fast_fast
// 6 -fast_slow
// 7 -slow_fast
// 8 -slow_slow
// 9 -done
// 10 - passed deadline
// initial state
[] (s=0) & (x<36) -> (x'=min(x+1,kx+1)) & (y'=min(y+1,ky+1));
[] (s=0) & (y<=deadline) -> 0.5 : (s'=1) + 0.5 : (s'=4);
[] (s=0) & (y<=deadline) -> 0.5 : (s'=2) + 0.5 : (s'=3);
[] (s=0) & (x<delay) -> (x'=min(x+1,kx+1)) & (y'=min(y+1,ky+1));
[] (s=0) & (y<=deadline) -> fast : (s'=1) + slow : (s'=4);
[] (s=0) & (y<=deadline) -> fast : (s'=2) + slow : (s'=3);
// fast_start
[] (s=1) & (x<36) -> (x'=min(x+1,kx+1)) & (y'=min(y+1,ky+1));
[] (s=1) & (y<=deadline) -> 0.5 : (s'=5) & (x'=0) + 0.5 : (s'=6) & (x'=0);
[] (s=1) & (x<delay) -> (x'=min(x+1,kx+1)) & (y'=min(y+1,ky+1));
[] (s=1) & (y<=deadline) -> fast : (s'=5) & (x'=0) + slow : (s'=6) & (x'=0);
// start_fast
[] (s=2) & (x<36) -> (x'=min(x+1,kx+1)) & (y'=min(y+1,ky+1));
[] (s=2) & (y<=deadline) -> 0.5 : (s'=5) & (x'=0) + 0.5 : (s'=7) & (x'=0);
[] (s=2) & (x<delay) -> (x'=min(x+1,kx+1)) & (y'=min(y+1,ky+1));
[] (s=2) & (y<=deadline) -> fast : (s'=5) & (x'=0) + slow : (s'=7) & (x'=0);
// start_slow
[] (s=3) & (x<36) -> (x'=min(x+1,kx+1)) & (y'=min(y+1,ky+1));
[] (s=3) & (y<=deadline) -> 0.5 : (s'=6) & (x'=0) + 0.5 : (s'=8) & (x'=0);
[] (s=3) & (x<delay) -> (x'=min(x+1,kx+1)) & (y'=min(y+1,ky+1));
[] (s=3) & (y<=deadline) -> fast : (s'=6) & (x'=0) + slow : (s'=8) & (x'=0);
// slow_start
[] (s=4) & (x<36) -> (x'=min(x+1,kx+1)) & (y'=min(y+1,ky+1));
[] (s=4) & (y<=deadline) -> 0.5 : (s'=7) & (x'=0) + 0.5 : (s'=8) & (x'=0);
[] (s=4) & (x<delay) -> (x'=min(x+1,kx+1)) & (y'=min(y+1,ky+1));
[] (s=4) & (y<=deadline) -> fast : (s'=7) & (x'=0) + slow : (s'=8) & (x'=0);
// fast_fast
[] (s=5) & (x<85) -> (x'=min(x+1,kx+1)) & (y'=min(y+1,ky+1));
[] (s=5) & (x>=76) & (y<=deadline) -> (s'=0) & (x'=0);
[] (s=5) & (x>=40) & (y<=deadline) -> (s'=9) & (x'=0);
[] (s=5) & (x>=76-delay) & (y<=deadline) -> (s'=9) & (x'=0);
// fast_slow
[] (s=6) & (x<167) -> (x'=min(x+1,kx+1)) & (y'=min(y+1,ky+1));
[] (s=6) & (x>=123) & (y<=deadline) -> (s'=9) & (x'=0);
[] (s=6) & (x>=159-delay) & (y<=deadline) -> (s'=9) & (x'=0);
// slow_fast
[] (s=7) & (x<167) -> (x'=min(x+1,kx+1)) & (y'=min(y+1,ky+1));
[] (s=7) & (x>=123) & (y<=deadline) -> (s'=9) & (x'=0);
[] (s=7) & (x>=159-delay) & (y<=deadline) -> (s'=9) & (x'=0);
// slow_slow
[] (s=8) & (x<167) -> (x'=min(x+1,kx+1)) & (y'=min(y+1,ky+1));
[] (s=8) & (x>=159) & (y<=deadline) -> (s'=0) & (x'=0);
[] (s=8) & (x>=123) & (y<=deadline) -> (s'=9) & (x'=0);
[] (s=8) & (x>=159-delay) & (y<=deadline) -> (s'=9) & (x'=0);
// move to deadline exceeded when y>=deadline
[] (y>=deadline) -> (s'=10);
[] (y>deadline) & (s<9) -> (s'=10) & (y'=0);
// done
[] (s=9) -> (s'=9);
// deadline exceeded

85
prism-examples/firewire/abst/firewire.nm
View File

@ -3,58 +3,75 @@
mdp
// wire delay
const int delay;
// probability of choosing fast and slow
const double fast;
const double slow = 1-fast;
// largest constant the clock of the system is compared to
const int kx = 167;
module abstract_firewire
// clock of the system
x : [0..168];
// clock
x : [0..kx+1];
// local state
s : [0..9];
// 0 - start_start
// 1 - fast_start
// 2 - start_fast
// 3 - start_slow
// 4 - slow_start
// 5 - fast_fast
// 6 - fast_slow
// 7 - slow_fast
// 8 - slow_slow
// 9 - done
// 0 -start_start
// 1 -fast_start
// 2 -start_fast
// 3 -start_slow
// 4 -slow_start
// 5 -fast_fast
// 6 -fast_slow
// 7 -slow_fast
// 8 -slow_slow
// 9 -done
// initial state
[] (s=0) & (x<36) -> (x'=min(x+1,kx+1));
[] (s=0) -> 0.5 : (s'=1) + 0.5 : (s'=4);
[] (s=0) -> 0.5 : (s'=2) + 0.5 : (s'=3);
[time] s=0 & x<delay -> (x'=min(x+1,kx+1));
[round] s=0 -> fast : (s'=1) + slow : (s'=4);
[round] s=0 -> fast : (s'=2) + slow : (s'=3);
// fast_start
[] (s=1) & (x<36) -> (x'=min(x+1,kx+1));
[] (s=1) -> 0.5 : (s'=5) & (x'=0) + 0.5 : (s'=6) & (x'=0);
[time] s=1 & x<delay -> (x'=min(x+1,kx+1));
[] s=1 -> fast : (s'=5) & (x'=0) + slow : (s'=6) & (x'=0);
// start_fast
[] (s=2) & (x<36) -> (x'=min(x+1,kx+1));
[] (s=2) -> 0.5 : (s'=5) & (x'=0) + 0.5 : (s'=7) & (x'=0);
[time] s=2 & x<delay -> (x'=min(x+1,kx+1));
[] s=2 -> fast : (s'=5) & (x'=0) + slow : (s'=7) & (x'=0);
// start_slow
[] (s=3) & (x<36) -> (x'=min(x+1,kx+1));
[] (s=3) -> 0.5 : (s'=6) & (x'=0) + 0.5 : (s'=8) & (x'=0);
[time] s=3 & x<delay -> (x'=min(x+1,kx+1));
[] s=3 -> fast : (s'=6) & (x'=0) + slow : (s'=8) & (x'=0);
// slow_start
[] (s=4) & (x<36) -> (x'=min(x+1,kx+1));
[] (s=4) -> 0.5 : (s'=7) & (x'=0) + 0.5 : (s'=8) & (x'=0);
[time] s=4 & x<delay -> (x'=min(x+1,kx+1));
[] s=4 -> fast : (s'=7) & (x'=0) + slow : (s'=8) & (x'=0);
// fast_fast
[] (s=5) & (x<85) -> (x'=min(x+1,kx+1));
[] (s=5) & (x>=76) -> (s'=0) & (x'=0);
[] (s=5) & (x>=40) -> (s'=9) & (x'=0);
[time] s=5 & (x<85) -> (x'=min(x+1,kx+1));
[] s=5 & (x>=76) -> (s'=0) & (x'=0);
[] s=5 & (x>=76-delay) -> (s'=9) & (x'=0);
// fast_slow
[] (s=6) & (x<167) -> (x'=min(x+1,kx+1));
[] (s=6) & (x>=123) -> (s'=9) & (x'=0);
[time] s=6 & x<167 -> (x'=min(x+1,kx+1));
[] s=6 & x>=159-delay -> (s'=9) & (x'=0);
// slow_fast
[] (s=7) & (x<167) -> (x'=min(x+1,kx+1));
[] (s=7) & (x>=123) -> (s'=9) & (x'=0);
[time] s=7 & x<167 -> (x'=min(x+1,kx+1));
[] s=7 & x>=159-delay -> (s'=9) & (x'=0);
// slow_slow
[] (s=8) & (x<167) -> (x'=min(x+1,kx+1));
[] (s=8) & (x>=159) -> (s'=0) & (x'=0);
[] (s=8) & (x>=123) -> (s'=9) & (x'=0);
[time] s=8 & x<167 -> (x'=min(x+1,kx+1));
[] s=8 & x>=159 -> (s'=0) & (x'=0);
[] s=8 & x>=159-delay -> (s'=9) & (x'=0);
// done
[] (s=9) -> (s'=9);
[] s=9 -> (s'=s);
endmodule
//reward structures
// time
rewards "time"
[time] true : 1;
endrewards
// number of rounds
rewards "rounds"
[round] true : 1;
endrewards
Write Preview
Loading…
Cancel
Save