From e97680d37dfd4e797891d732b272aeed0a38c9e5 Mon Sep 17 00:00:00 2001 From: dehnert Date: Thu, 17 Oct 2013 22:20:17 +0200 Subject: [PATCH] Added counterexample property files for some models. Former-commit-id: 1cd16d0aca9d3c23bfa04fd0c8e0c8dc62c808e3 --- examples/mdp/consensus/coin.cexprop | 1 + examples/mdp/csma/csma.cexprop | 1 + examples/mdp/firewire/impl/firewire.cexprop | 1 + examples/mdp/wlan/wlanX_1.cexprop | 1 + examples/mdp/wlan/wlanX_2.cexprop | 1 + 5 files changed, 5 insertions(+) create mode 100644 examples/mdp/consensus/coin.cexprop create mode 100644 examples/mdp/csma/csma.cexprop create mode 100644 examples/mdp/firewire/impl/firewire.cexprop create mode 100644 examples/mdp/wlan/wlanX_1.cexprop create mode 100644 examples/mdp/wlan/wlanX_2.cexprop diff --git a/examples/mdp/consensus/coin.cexprop b/examples/mdp/consensus/coin.cexprop new file mode 100644 index 000000000..bb60f986d --- /dev/null +++ b/examples/mdp/consensus/coin.cexprop @@ -0,0 +1 @@ +P<0.4 [ F finished & all_coins_equal_1 ] diff --git a/examples/mdp/csma/csma.cexprop b/examples/mdp/csma/csma.cexprop new file mode 100644 index 000000000..fd4346176 --- /dev/null +++ b/examples/mdp/csma/csma.cexprop @@ -0,0 +1 @@ +P<0.5 [ !collision_max_backoff U all_delivered ] diff --git a/examples/mdp/firewire/impl/firewire.cexprop b/examples/mdp/firewire/impl/firewire.cexprop new file mode 100644 index 000000000..02d43560f --- /dev/null +++ b/examples/mdp/firewire/impl/firewire.cexprop @@ -0,0 +1 @@ +P<0.5 [F elected] diff --git a/examples/mdp/wlan/wlanX_1.cexprop b/examples/mdp/wlan/wlanX_1.cexprop new file mode 100644 index 000000000..4c3a40fd8 --- /dev/null +++ b/examples/mdp/wlan/wlanX_1.cexprop @@ -0,0 +1 @@ +P<0.5 [ F oneCollision ] diff --git a/examples/mdp/wlan/wlanX_2.cexprop b/examples/mdp/wlan/wlanX_2.cexprop new file mode 100644 index 000000000..1dad8767d --- /dev/null +++ b/examples/mdp/wlan/wlanX_2.cexprop @@ -0,0 +1 @@ +P<0.1 [ F twoCollisions ]