* ************************************************************
* Course: Verification
* Kim G.Larsen, Spring 2000
*
* Joost-Pieter Katoen: Concepts, Algorithms and Tools for Model Checking
* Exercise 24 (page 185)
*
*		    ----------------------------	
*		     Dijkstra's Mutex Algorithm
*		    ----------------------------
*
* M. Oliver Möller <omoeller@brics.dk>
*
* ************************************************************
* ****************   2  processes ****************************
* ************************************************************
*

** ****************************************
**  Model of the 2 Processes
** ****************************************

**** Boolean Vector B[1..2]
** Boolean Memory Cell B[1]
agent B_1_true = readB_1_true.B_1_true  + 'setB_1_true.B_1_true + 'setB_1_false.B_1_false ;
agent B_1_false = readB_1_false.B_1_false  + 'setB_1_true.B_1_true + 'setB_1_false.B_1_false ;
** Boolean Memory Cell B[2]
agent B_2_true = readB_2_true.B_2_true  + 'setB_2_true.B_2_true + 'setB_2_false.B_2_false ;
agent B_2_false = readB_2_false.B_2_false  + 'setB_2_true.B_2_true + 'setB_2_false.B_2_false ;
**** 
**** Boolean Vector C[1..2]
** Boolean Memory Cell C[1]
agent C_1_true = readC_1_true.C_1_true  + 'setC_1_true.C_1_true + 'setC_1_false.C_1_false ;
agent C_1_false = readC_1_false.C_1_false  + 'setC_1_true.C_1_true + 'setC_1_false.C_1_false ;
** Boolean Memory Cell C[2]
agent C_2_true = readC_2_true.C_2_true  + 'setC_2_true.C_2_true + 'setC_2_false.C_2_false ;
agent C_2_false = readC_2_false.C_2_false  + 'setC_2_true.C_2_true + 'setC_2_false.C_2_false ;
**** 
**** Bounded Integer K in [1..2]
agent K_1 = readK_1.K_1 + 'setK_1.K_1 + 'setK_2.K_2 ;
agent K_2 = readK_2.K_2 + 'setK_1.K_1 + 'setK_2.K_2 ;
**** 
agent Memory = B_1_true | C_1_true | B_2_true | C_2_true | ( tau.K_1 + tau.K_2 ) ;
agent Empty = 'enter_1.Occupied + 'enter_2.Occupied ;
agent Occupied = 'enter_1.Fail + 'enter_2.Fail +  'leave.Empty ;
agent Fail = fail.Fail ; 
**
** Process 1
**
agent Process_1 = setB_1_false.L_1 ;
agent L_1 = 'readK_1.Else_1  + 'readK_2.Then_1 ;  ; 
agent Then_1 = setC_1_true.Split_1 ; 
agent Split_1 = 'readK_1.Split_1_1 + 'readK_2.Split_1_2 ; 
agent Split_1_1 = 'readB_1_true.setK_1.L_1 + 'readB_1_false.L_1 ;
agent Split_1_2 = 'readB_2_true.setK_1.L_1 + 'readB_2_false.loop_1.L_1 ;
agent Else_1 = setC_1_false.Query_1_2 ;
agent Query_1_2 = 'readC_2_false.L_1 + 'readC_2_true.Query_1_3 ; 
agent Query_1_3 = enter_1.bell_1.leave.setC_1_true.setB_1_true.Process_1 ; 
**
** Process 2
**
agent Process_2 = setB_2_false.L_2 ;
agent L_2 = 'readK_2.Else_2  + 'readK_1.Then_2 ;  ; 
agent Then_2 = setC_2_true.Split_2 ; 
agent Split_2 = 'readK_1.Split_2_1 + 'readK_2.Split_2_2 ; 
agent Split_2_1 = 'readB_1_true.setK_2.L_2 + 'readB_1_false.L_2 ;
agent Split_2_2 = 'readB_2_true.setK_2.L_2 + 'readB_2_false.L_2 ;
agent Else_2 = setC_2_false.Query_2_1 ;
agent Query_2_1 = 'readC_1_false.L_2 + 'readC_1_true.Query_2_3 ; 
agent Query_2_3 = enter_2.bell_2.leave.setC_2_true.setB_2_true.Process_2 ; 

set SyncActions = { setB_1_true, setB_1_false, readB_1_true, readB_1_false, setC_1_true, setC_1_false, readC_1_true, readC_1_false, setB_2_true, setB_2_false, readB_2_true, readB_2_false, setC_2_true, setC_2_false, readC_2_true, readC_2_false, setK_1, readK_1, enter_1, setK_2, readK_2, enter_2, leave }; 

agent System = ( Memory | Process_1 | Process_2 | Empty )\SyncActions ;

** ****************************************
** On the model:
** Process i has observable actions bell_i, issued when in the critical
** region. In addition, process 1 has the action "loop_1" at a strategic
** place.
** Entering and leaving the critical region is synchronized with a process
** "Empty", that mutates to "Occupied" and further to "Fail", if another
** enter happens before an exit.
** Fail can execute action "fail".
** Mutex holds, if "fail" is never (strongly) enabled:
** 
** ************************************************************ 
** 
prop Mutex = ~min(Z.<fail>T | <->Z) ;
**
** ****************************************
** Individual Starvation
** ****************************************
** If suffices to check two things:
** (a) It is not possible for the system to deadlock
**
prop DeadlockFree = max(Z.<->T & [-]Z); ** true
**
** (b) It is possible to reach a situation, from where bell_1 is never
** weakly enabled, readK_1 is never weakly enabled (but loop_1 is!)
**
prop Infinitely_Delayed_1 = min(X.max(Y.[[bell_1]]F & [[readK_1]]F & <<loop_1>>T & <->Y ) | <->X);
**
** This gives us the loop, which is _fair_:
** The only way to leave it would be via readK_1, but this is never enabled.
** **********************************************************************