Browse Source

Adapted the pctl files according to our format.

tempestpy_adaptions
dehnert 12 years ago
parent
commit
0f545630eb
  1. 6
      examples/dtmc/crowds/crowds.pctl
  2. 8
      examples/dtmc/die/die.pctl
  3. 6
      examples/dtmc/synchronous_leader/leader.pctl
  4. 10
      examples/mdp/asynchronous_leader/leader.pctl
  5. 16
      examples/mdp/consensus/coin.pctl
  6. 24
      examples/mdp/two_dice/two_dice.pctl

6
examples/dtmc/crowds/crowds.pctl

@ -1,3 +1,3 @@
P=? [ F "observe0Greater1" ]
P=? [ F "observeIGreater1" ]
P=? [ F "observeOnlyTrueSender" ]
P=? [ F observe0Greater1 ]
P=? [ F observeIGreater1 ]
P=? [ F observeOnlyTrueSender ]

8
examples/dtmc/die/die.pctl

@ -1,4 +1,4 @@
P=? [ F "one" ]
P=? [ F "two" ]
P=? [ F "three" ]
R=? [ F "done" ]
P=? [ F one ]
P=? [ F two ]
P=? [ F three ]
R=? [ F done ]

6
examples/dtmc/synchronous_leader/leader.pctl

@ -1,3 +1,3 @@
P=? [ F "elected" ]
P=? [ F<=(4*(N+1)) "elected" ]
R=? [ F "elected" ]
P=? [ F elected ]
P=? [ F<=(4*(N+1)) elected ]
R=? [ F elected ]

10
examples/mdp/asynchronous_leader/leader.pctl

@ -1,8 +1,8 @@
Pmin=? [ F "elected" ]
Pmin=? [ F elected ]
const int K = 25;
Pmin=? [ F<=K "elected" ]
Pmax=? [ F<=K "elected" ]
Pmin=? [ F<=K elected ]
Pmax=? [ F<=K elected ]
Rmin=? [ F "elected" ]
Rmax=? [ F "elected" ]
Rmin=? [ F elected ]
Rmax=? [ F elected ]

16
examples/mdp/consensus/coin.pctl

@ -1,20 +1,20 @@
// C1 (with probability 1, all N processes finish the protocol)
Pmin=? [ F "finished" ]
Pmin=? [ F finished ]
// C2 (minimum probability that the protocol finishes with all coins equal to v) (v=1,2)
// Results are same for v=1 and v=2 by symmetry
// Analytic bound is (K-1)/(2*K)
Pmin=? [ F "finished"&"all_coins_equal_0" ]
Pmin=? [ F "finished"&"all_coins_equal_1" ]
Pmin=? [ F finished & all_coins_equal_0 ]
Pmin=? [ F finished & all_coins_equal_1 ]
// Max probability of finishing protocol with coins not all equal
Pmax=? [ F "finished"&!"agree" ]
Pmax=? [ F finished & !agree ]
// Min/max probability of finishing within k steps
Pmin=? [ F<=k "finished" ]
Pmax=? [ F<=k "finished" ]
Pmin=? [ F<=k finished ]
Pmax=? [ F<=k finished ]
// Min/max expected steps to finish
Rmin=? [ F "finished" ]
Rmax=? [ F "finished" ]
Rmin=? [ F finished ]
Rmax=? [ F finished ]

24
examples/mdp/two_dice/two_dice.pctl

@ -1,13 +1,13 @@
Pmin=? [ F "two" ]
Pmax=? [ F "two" ]
Pmin=? [ F "three" ]
Pmax=? [ F "three" ]
Pmin=? [ F "four" ]
Pmax=? [ F "four" ]
Pmin=? [ F "five" ]
Pmax=? [ F "five" ]
Pmin=? [ F "six" ]
Pmax=? [ F "six" ]
Pmin=? [ F two ]
Pmax=? [ F two ]
Pmin=? [ F three ]
Pmax=? [ F three ]
Pmin=? [ F four ]
Pmax=? [ F four ]
Pmin=? [ F five ]
Pmax=? [ F five ]
Pmin=? [ F six ]
Pmax=? [ F six ]
Rmin=? [ F "done" ]
Rmax=? [ F "done" ]
Rmin=? [ F done ]
Rmax=? [ F done ]
Loading…
Cancel
Save