- 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.

- 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.

Except where otherwise noted, content on this wiki is licensed under the following license: CC Attribution-Noncommercial-Share Alike 3.0 Unported