IOA Examples

You can find the IOA toolset in the directory

/vol/itt/ioa

(both on the cs and the sci domain). The syntax checker works. You can see this by trying

setenv PATH /vol/itt/ioa/bin:$PATH 
ioaCheck /vol/itt/ioa/Examples/Fibonacci01/Fibonacci01.ioa

To play with the simulator, copy Fibonacci.ioa to a writable directory, go there and run

sim 10 Fibonacci.ioa | more

Another example you can try is the division algorithm we discussed during the course. Copy the ioa file to a writable directory, change the code to initialize the variables x and y

    x : Int := 40,
    y : Int := 11,

and run

sim 100 -outputState division.ioa | more

to discover that 40 = 3*11 + 7.

For a list of allowable flags just run sim. A detailled manual for the simulator is available at the IOA website.

Below you will find some examples of IOA specifications, some of which were discussed during the course on Protocol Validation:

A two state switch.
The same switch in predicative style.
An adder (this is a small variation of the adder described in the IOA manual, intended to give a trivial example of an inductive property).
An I/O automaton that computes the square root of two natural numbers.
A solution to the channel specification problem. The solutions refers to an LSL module PortSpec.lsl describing the Ports datatype.
A number of solutions to the jobshop specification problem.
An I/O automaton that computes the integer quotient of two positive integers.
A specification of a lossy channel together with an auxiliary LSL trait Subsequence.lsl that defines a subsequence predicate.
A specification of the Le Lann, Chang and Roberts leader election protocol together with an auxiliary LSL trait RingIndex.lsl that defines the datatype RingIndex.
A specification of the elevator next to my office together with an auxiliary LSL trait Floors.lsl that defines the Floors in our building.

Last change made on 1/6/5 by Frits Vaandrager.