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.

[Sample Code]

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
Except where otherwise noted, content on this wiki is licensed under the following license: CC Attribution-Noncommercial-Share Alike 3.0 Unported
Recent changes RSS feed Donate Powered by PHP Valid XHTML 1.0 Valid CSS Driven by DokuWiki