* 
* Course: Verification
* Kim G.Larsen, Spring 2000
*
* Demo for the Concurency Workbench
*
* M. Oliver Möller <omoeller@brics.dk>
* BEGUN: 10/04/2000
*

agent GoodMachine = tau.Seller;
agent Seller = 'coffee.0 + 'tea.0 ;

agent BadMachine = tau.'coffee.0 + tau.'tea.0 ;

agent Consumer = tea.Consumer + coffee.Consumer ; 

set Drinks = {tea, coffee} ;

* ****************************************

agent Blur = a.Blur + b.Blur;
agent BlurWeak = a.tau.BlurWeak + b.tau.BlurWeak ;
agent Pit = a.Pit + b.0;

prop Allways_a = max(X.(<a>T & [-]X )) ;
prop Allways_b = max(X.(<b>T & [-]X )) ;

prop WeakAllways_a = max(X.(<<a>>T & [-]X )) ;
prop WeakAllways_b = max(X.(<<b>>T & [-]X )) ;

** **************************************************

agent M_0 = readM_0.M_0 + 'setM_0.M_0 + 'setM_1.M_1 + 'setM_2.M_2 ;
agent M_1 = readM_1.M_1 + 'setM_0.M_0 + 'setM_1.M_1 + 'setM_2.M_2 ;
agent M_2 = readM_2.M_2 + 'setM_0.M_0 + 'setM_1.M_1 + 'setM_2.M_2 ;