This package contains the following files: 

- Specification of GDH as part of Cliques: 

  cliques.maude

- Examples of protocol runs and analysis using search and model checking: 

  examples.maude
  examples.out (execution protocol)

We assume that Maude 2.0 has been installed.

Instructions to execute the examples:

   1. start the Maude system
   2. type "in cliques.maude" to load the formal specification
   3. type "examples.maude" to execute all examples
      (the search and model checking examples require some time to terminate)