This package contains the following files: 

 Common data types and operations

     natutil.maude  	--- natural number and operations
     proc.maude     	--- processes (daemons)
     agent.maude    	--- agents (potential clients)
     group.maude    	--- logical groups
     state.maude    	--- distributed system state
     mode.maude     	--- message delivery modes


 Configuration layer: 

     conf.maude          --- configurations, i.e. instances of process 
     			 --- membership in connected component
     cmessage.maude      --- configuration layer messages
     constraints.maude   --- delivery constraints
     capi.maude          --- configurational level API
     ccommon.maude       --- common for the following two modes
     coperational.maude  --- normal operational mode
     cchange.maude       --- transitional mode
     cspread.maude       --- combined configurational layer specification


 Group layer:

     view.maude          --- views, i.e instances of agent membership in groups
     gmessage.maude      --- group layer messages
     gapi.maude          --- group layer API
     spread.maude        --- combined group layer specification


 Flush layer:

     fmessage.maude      --- flush layer messages
     fapi.maude          --- flush layer API
     flushspread.maude   --- combined Flush layer specification


 Secure layer:

     cliques.maude       --- Cliques toolkit specification
     smessage.maude      --- secure layer messages
     sapi.maude          --- secure layer API
     groupvar.maude      --- group specific variables
     assockey.maude	 --- keyid specific variables
     assocmembset.maude	 --- associated keyid-members
     securespread.maude  --- combined Secure specification


 Load all layers: 

     all.maude 


 Controlling the Execution: 

     controller.maude     --- a simple controller language
     test.maude           --- prelude for configuration layer testing
     gtest.maude          --- prelude for group layer testing
     ftest.maude          --- prelude for flush layer testing
     stest.maude          --- prelude for secure layer testing


   Examples : 

     stestvs1.maude 	--- VS Semantics, data blocking, eager rekey
     	R: stestvs1.out	
     stestvs2.maude 	--- VS Semantics, non-blocking data, eager rekey
     	R: stestvs2.out	
     stestevs1.maude	--- EVS Semantics, eager rekey
     	R: stestevs1.out	
     stestevs2.maude	--- EVS Semantics, key caching
     	R: stestevs2.out	
     stestevs3.maude 	--- EVS Semantics, lazy rekey
     	R: stestevs3.out	
     stestevs4.maude 	--- EVS Semantics, fresh secure message
     	R: stestevs4.out	
     stestevs5.maude 	--- EVS Semantics, reuqested sending view
     	R: stestevs5.out	
     stestevs6.maude 	--- Combined Groups (EVS/VS Semantics)
     	R: stestevs6.out	


We assume that Maude 2.0 has been installed.


Instructions to execute the examples:

   1. start the Maude system
   2. type "in all.maude" to load the formal specification
   3. type "stestvs1.maude" to execute the first example 
      and correspondingly for the others