|
127
|
1 MODULE main
|
|
|
2 VAR
|
|
|
3 semaphore : boolean;
|
|
|
4 proc1 : process user(semaphore);
|
|
|
5 proc2 : process user(semaphore);
|
|
|
6 ASSIGN
|
|
|
7 init(semaphore) := FALSE;
|
|
|
8 SPEC AG ! (proc1.state = critical & proc2.state = critical)
|
|
|
9 SPEC AG (proc1.state = entering -> AF proc1.state = critical)
|
|
|
10 MODULE user(semaphore)
|
|
|
11 VAR
|
|
|
12 state : {idle, entering, critical, exiting};
|
|
|
13 ASSIGN
|
|
|
14 init(state) := idle;
|
|
|
15 next(state) :=
|
|
|
16 case
|
|
|
17 state = idle : {idle, entering};
|
|
|
18 state = entering & !semaphore : critical;
|
|
|
19 state = critical : {critical, exiting};
|
|
|
20 state = exiting : idle;
|
|
|
21 TRUE : state ;
|
|
|
22 esac;
|
|
|
23 next(semaphore) :=
|
|
|
24 case
|
|
|
25 state = entering : TRUE;
|
|
|
26 state = exiting : FALSE;
|
|
|
27 TRUE : semaphore;
|
|
|
28 esac;
|
|
|
29 FAIRNESS
|
|
|
30 running
|
