move everything out of trunk

[lttv.git] / trunk / verif / Spin / Test / abp

diff --git a/trunk/verif/Spin/Test/abp b/trunk/verif/Spin/Test/abp
deleted file mode 100755 (executable)
index 0b61890..0000000
--- a/trunk/verif/Spin/Test/abp
+++ /dev/null
@@ -1,47 +0,0 @@
-/*
- *  a simple example of the use of inline's
- *  (requires Spin version 3.2 or later)
- *
- */
-
-mtype = { msg0, msg1, ack0, ack1 };
-
-chan sender = [1] of { mtype };
-chan receiver = [1] of { mtype };
-
-inline phase(msg, good_ack, bad_ack)
-{
-       do
-       :: sender?good_ack -> break
-       :: sender?bad_ack
-       :: timeout -> 
-               if
-               :: receiver!msg;
-               :: skip /* lose message */
-               fi;
-       od
-}
-
-inline recv(cur_msg, cur_ack, lst_msg, lst_ack)
-{
-       do
-       :: receiver?cur_msg -> sender!cur_ack; break /* accept */
-       :: receiver?lst_msg -> sender!lst_ack
-       od;
-} 
-
-active proctype Sender()
-{
-       do
-       :: phase(msg1, ack1, ack0);
-          phase(msg0, ack0, ack1)
-       od
-}
-
-active proctype Receiver()
-{
-       do
-       :: recv(msg1, ack1, msg0, ack0);
-          recv(msg0, ack0, msg1, ack1)
-       od
-}