This package contains the following files: 

   Common data types and operations

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

   Spread 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

 Spread group layer:

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

 Flush Spread layer:

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

 Secure Spread layer:

     cliques.maude       --- Cliques toolkit specification
     smessage.maude      --- secure layer messages
     sapi.maude          --- secure layer API
     groupvar.maude      --- group specific variables
     securespread.maude  --- combined Secure Spread specification

 Load all layers (Spread, Flush Spread, and Secure Spread): 

     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 using Spread configuration layer: 

     test1.maude result: test1.out 
     test2.maude result: test2.out 
     test3.maude result: test3.out 
     test4.maude result: test4.out 
     test5.maude result: test5.out 
     test6.maude result: test6.out 
     test7.maude result: test7.out 
     test8.maude result: test8.out 
     test9.maude result: test9.out 
     test10.maude result: test10.out 
     test11.maude result: test11.out 
     test12.maude result: test12.out 
     test13.maude result: test13.out 
     test14.maude result: test14.out 
     test15.maude result: test15.out 

   Examples using Spread group layer: 

     gtest1.maude result: gtest1.out 
     gtest2.maude result: gtest2.out 
     gtest3.maude result: gtest3.out 
     gtest4.maude result: gtest4.out 
     gtest5.maude result: gtest5.out 

   Examples using Spread flush layer: 

     ftest1.maude result: gtest1.out 
     ftest2.maude result: gtest2.out 
     ftest3.maude result: gtest3.out 
     ftest4.maude result: gtest4.out 

   Examples using Spread secure layer: 

     stest1.maude result: stest1.out 
     stest2.maude result: stest2.out 
     stest3.maude result: stest3.out 
     stest4.maude result: stest4.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 "test1.maude" to execute the first example
      and correspondingly for the others