Details of Use Cases

• Step 1: If the repository has what you want, open it and go to Step 3.
• Step 2: Draw a Büchi automaton diagram (in seconds, if you already have it in mind).
• Step 3: Drag and drop to reshape the diagram to your preferred layout.
• Step 4: Print the diagram to a PDF file, then do things as usual.

Whether a hand-drawn automaton is correct, with respect to a QPTL (or PTL if it suffices) formula, can be verified using either of the following two methods:

• Method One
  • Step 1: Translate the formula into an equivalent Büchi automaton.
  • Step 2: Test the equivalence between the machine-translated and the hand-drawn automata.
• Method Two
  • Step 1: In the automaton editor window, choose the “Equivalence with a Formula” test and follow the instructions.

• Step 1: Draw a smaller Büchi automaton.
• Step 2: Check if it is equivalent to a previous correct automaton.
• Step 3: Repeat 1-2 until you are happy with the number of states.

Though it is essentially a trial-and-error process, the equivalence test provided by GOAL will greatly ease the pain.

• Step 1: Draw a specification automaton.
• Step 2: Export the automaton as Promela code.
• Step 3: Copy-and-paste the Promela code to SPIN's model file as the “never claim”.
• Step 4: Continue the model checking procedure as usual.

• Step 1: Implement the complementation algorithm in any programming language. Lets call the implementation Impl.
• Step 2: Make the algorithm available in the GOAL command-line mode by extending the ComplementCommand extension point and delegating the complementation task to Impl.
• Step 3: Check the correctness of Impl by writing a GOAL script that
  • generates random Büchi automata,
  • complements the automata by Impl and other complementation algorithms provided by GOAL,
  • compares the results by equivalence checking, and
  • outputs any counterexample.

The random automata generation and the equivalence checking are built-in functions of GOAL.

[Sample Code]

• Step 1. Change the preference “Find in the repository” in the Translation section to “Exact Match” or “Unify”.
• Step 2. Enable the preference “Use the remote repository”.
• Step 3. Translate any QPTL formula. If there is a match in the Büchi Store, GOAL will download the automaton from the store and apply appropriate renaming automatically.

Other uses are, of course, possible.