This package contains the following files: 

   * README instructions on how to run the examples 

   * sectrace.maude: specification of the sectrace protocol

   * Examples:

      - basic-test-1.maude
        basic-test-1.sol

      - basic-test-2.maude
        basic-test-2.sol

      - ext-test-seq-c1-c2.maude
        ext-test-seq-c1-c2.sol

      - ext-test-seq-c2-c1.maude
        ext-test-seq-c2-c1.sol

      - ext-test-inter.maude
        ext-test-inter.trace1
        ext-test-inter.trace2
        ext-test-inter.trace3
        ext-test-inter.trace4

We assume that Maude 2.0 has been installed.

Instructions to execute the examples:

   1. start the Maude system
   2. type "in sectrace.maude" to load the formal specification
   3. type "basic-test-1.maude" to execute the first example
      and correspondingly for the others

Note that the example "ext-test-inter.maude" involves 
search and modelchecking and may take quite a while
even on a fast machine.