A minimal protocol for testing the partial order reductions.
This commit is contained in:
parent
9010e37c33
commit
66bad3856c
29
spdl/onetrace.spdl
Normal file
29
spdl/onetrace.spdl
Normal file
@ -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);
|
Loading…
Reference in New Issue
Block a user