|
0
|
1 '$define' progress(Cr1,Crit,Conc):-
|
|
|
2 #(Cr1=true),Crit
|
|
|
3 && @ (#(Cr1=false),Conc).
|
|
|
4
|
|
|
5 '$define' ( exclusion(Id,Id2,T,Cr1,Cr2,Crit,Conc):- H )
|
|
|
6 '$clause' ( H :-
|
|
|
7 Cr1=true,
|
|
|
8 enter(Id,Id2,T,Cr1,Cr2)
|
|
|
9 && progress(Cr1,Crit,Conc)
|
|
|
10 && @ H) .
|
|
|
11
|
|
|
12 enter(Id,Id2,T,Cr1,Cr2) :-
|
|
|
13 Cr2=true,T=Id2,@Cr1=false,
|
|
|
14 @enter(Id,Id2,T,Cr1,Cr2).
|
|
|
15 enter(Id,Id2,T,Cr1,Cr2) :-
|
|
|
16 Cr2=true,T=Id,@Cr1=true,@T=Id,
|
|
|
17 @trust(Id,Id2,T,Cr1,Cr2).
|
|
|
18 enter(Id,Id2,T,Cr1,Cr2) :-
|
|
|
19 Cr2=false,@Cr1=true,skip.
|
|
|
20
|
|
|
21 trust(Id,Id2,T,Cr1,Cr2) :-stable(T),
|
|
|
22 Cr2=true,@Cr1=true,
|
|
|
23 @trust(Id,Id2,T,Cr1,Cr2).
|
|
|
24 trust(Id,Id2,T,Cr1,Cr2) :-
|
|
|
25 Cr2=false,@Cr1=true,skip.
|
|
|
26
|
|
|
27
|
|
|
28 dekker:-T=0,Cr1=true,Cr2=true,
|
|
|
29 exclusion(0,1,T,Cr1,Cr2,critical(0),concurrent(0)),
|
|
|
30 exclusion(1,0,T,Cr2,Cr1,critical(1),concurrent(1)).
|
|
|
31
|
|
|
32 critical(Id):-length(2),
|
|
|
33 keep((write('critical-region'),write(Id),nl)).
|
|
|
34
|
|
|
35 concurrent(Id):-length(3),
|
|
|
36 keep((write('concurrent-region'),write(Id),nl)).
|
|
|
37
|
