Added counterexample property files for some models.

Former-commit-id: 1cd16d0aca
11 years ago · e97680d37d
5 changed files with 5 additions and 0 deletions
--- a/examples/mdp/consensus/coin.cexprop
+++ b/examples/mdp/consensus/coin.cexprop
@ -0,0 +1 @@
+P<0.4 [ F finished & all_coins_equal_1 ]
--- a/examples/mdp/csma/csma.cexprop
+++ b/examples/mdp/csma/csma.cexprop
@ -0,0 +1 @@
+P<0.5 [ !collision_max_backoff U all_delivered ]
--- a/examples/mdp/firewire/impl/firewire.cexprop
+++ b/examples/mdp/firewire/impl/firewire.cexprop
@ -0,0 +1 @@
+P<0.5 [F elected]
--- a/examples/mdp/wlan/wlanX_1.cexprop
+++ b/examples/mdp/wlan/wlanX_1.cexprop
@ -0,0 +1 @@
+P<0.5 [ F oneCollision ]
--- a/examples/mdp/wlan/wlanX_2.cexprop
+++ b/examples/mdp/wlan/wlanX_2.cexprop
@ -0,0 +1 @@
+P<0.1 [ F twoCollisions ]