From 66bad3856cd81512e813e47bf0c5963f37906b5f Mon Sep 17 00:00:00 2001 From: ccremers Date: Wed, 3 Mar 2004 18:59:23 +0000 Subject: [PATCH] A minimal protocol for testing the partial order reductions. --- spdl/onetrace.spdl | 29 +++++++++++++++++++++++++++++ 1 file changed, 29 insertions(+) create mode 100644 spdl/onetrace.spdl diff --git a/spdl/onetrace.spdl b/spdl/onetrace.spdl new file mode 100644 index 0000000..26ba9c1 --- /dev/null +++ b/spdl/onetrace.spdl @@ -0,0 +1,29 @@ +usertype String; + +const Alice,Bob,Charlie: Agent; +const Hallo: String; + +protocol onetrace(I) +{ + role I + { + var input: String; + + read_1(I,I, input); + send_2(I,I, Hallo); + read_3(I,I, input); + } +} + +run onetrace.I(Alice); +run onetrace.I(Alice); +run onetrace.I(Alice); +run onetrace.I(Alice); + +run onetrace.I(Alice); +run onetrace.I(Alice); +run onetrace.I(Alice); +run onetrace.I(Alice); + +run onetrace.I(Alice); +run onetrace.I(Alice);