# Details of Use Cases

## A. Preparing Büchi automaton diagrams for slides/papers/homework

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

## B. Checking correctness of a hand-drawn Büchi automaton

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.

## C. “Hand-optimization” of a specification Büchi automaton

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

## D. Combining GOAL with SPIN

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

## E. Checking correctness of a Büchi complementation algorithm

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

## F. Utilizing the Büchi Store

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

goal/usecase.txt · Last modified: 2012/02/22 01:59 by mht208