/* Example of Transition system in SPIN */
/* Refer to slides for TS graphic */
/* Author:  Nathalie Cauchi- nathalie.cauchi@cs.ox.ac.uk */

byte state = 1; /* Set initial state */
bool a = true, b = false, c = false; /* Labelling */
active proctype P() /* Definition of TS */
{
do
::atomic{ state==1-> state=3; a=false; b=true; c=true}
::atomic{ state==1-> state=4; a=false; b=true; c=false}
::atomic{ state==4-> state=2; a=false; b=false; c=true}
::atomic{ state==4-> state=3; a=false; b=true; c=true}
::atomic{ state==4-> state=5; a=true; b=true; c=true}
::atomic{ state==2-> state=4; a=false; b=true; c=true}
::atomic{ state==3-> state=4; a=false; b=true; c=false}
::atomic{ state==5-> state=4; a=false; b=true; c=false}
::atomic{ state==5-> state=5; a=true; b=true; c=true}
od
}
ltl F1 {<>[] (c||b)}
/*
ltl F2 {<>[] c||b}
ltl F3 {<>[] c}
*/