Contracts

The Argos compiler has several features that make working with observers and contracts easier, if some conventions are respected. First, name all your Error states ERROR, and let all transitions leading to it emit a error signal, preferably err. To check a contract, call the assumption and the guarantee observer in parallel to the program, and let them emit different error signals, e.g. errA and errG. Then, put another automaton in parallel which emits output fail if ~errA&errG is true. Then, call the ArgosCompiler with option -contract. It will then check if a transition which emits fail is reachable in the flattened program, and if so, emit a trace leading to it.

Download the source code for the tram example from TR-2006-10.

Télécharchez le code source pour le code source du l'exemple du papier JFDLPA.

Back to the ArgosCompiler page

Back to my home page