This package contains the following files: 

   1. README instructions on how to run the examples 
   2. plan-syntax.m: specification of the programming language syntax 
   3. plan-sorts.m: various sorts (values, nonvalues, etc.) used in the specification 
   4. plan-network.m: network related sorts/operations 
   5. plan-semantics.m: operational semantics of the language 
   6. p.m: loads the entire specification, i.e. all the files above
   7. topologies.m: definitions of two different network topologies 
   8. semantics-runs.m: execution of examples not requiring a network 
   9. find-examples.m: definitions of two active network programs 
  10. find-runs.m: execution of these programs on the above topologies 

We assume that Maude 2.0 has been installed.

Instructions to execute the examples:

   1. start the Maude system
   2. type "in p.m" to load the formal specification
   3. type "semantics-runs.m" to execute the simple examples
      (topologies.m is loaded automatically for some examples)
   4. type "in find-examples.m" to load the two active network programs
   5. type "in find-runs.m" to execute both programs in each of the two networks