TRecS (Types for RECursion Schemes): Type-Based Model Checker for Higher-Order Recursion Schemes

Enter a recursion scheme and a specification in the box below, and press the "submit" button. Examples are given below. Currently, our model checker only accepts deterministic Buchi automata with a trivial acceptance condition.

You can test only small examples on this page. Consult us (Naoki Kobayashi) if you would like to get source programs of TRecS and run it on your machine.

Some examples are given below. More examples are available here .

Example 1

%BEGING    /*** Rewring rules of a recursion scheme. Non-terminal must start with a capital letter. ***/
S -> F c.  /*** The non-terminal of the first rule is interpreted as the start symbol. ***/
F x -> a x (F (b x)).  /*** Unbounded names ("a", "b" in this rule) are interpreted as terminals. ***/
%ENDG

%BEGINA    /*** Transition rules of a Buchi tree automaton (where all the states are final). ***/
q0 a -> q0 q0. /*** The first state is interpreted as the initial state. **/
q0 b -> q1.
q1 b -> q1.
q0 c -> .
q1 c -> .
%ENDA

Example 2

/*** An example taken from POPL09 paper, which creates and accesses two files ***/
%BEGING
S -> Newr C1.
C1 x -> Neww (C2 x).
C2 x y -> F x y end.
F x y k -> br (Close x (Close y k)) (Read x (Write y (F x y k))).
I x y -> x y.
K x y -> y.
Newr k -> br (newr (k I)) (k K).
Neww k -> br (neww (k I)) (k K).
Close x k -> x close k.
Read x k -> x read k.
Write y k -> y write k.
%ENDG

%BEGINA
q0 br -> q0 q0.
qr br -> qr qr.
qw br -> qw qw.
qrw br -> qrw qrw.
q0 newr -> qr.
qr read -> qr.
qr close -> qc.
q0 neww -> qw.
qw write -> qw.
qw close -> qc.
qw newr -> qrw.
qr neww -> qrw.
qrw read -> qrw.
qrw write -> qrw.
qrw close -> qrw.
qc end ->.
q0 end ->.
qrw end ->.
%ENDA

Example 3

/*** An example taken from POPL09 paper, which acquires and releases a lock. ***/
%BEGING
S -> br (New (F0 end)) (New (F1 end)).
F0 k x -> C0 x k.
F1 k x -> Lock x (C1 x k).
C0 x k -> k.
C1 x k -> Unlock x k.
New k -> br (newl (k I)) (k K).
I x y -> x y.
K x y -> y.
Lock x k -> x lock k.
Unlock x k -> x unlock k.
%ENDG

%BEGINA
q0 br -> q0 q0.
q1 br -> q1 q1.
q2 br -> q2 q2.
q0 newl -> q1.
q1 lock -> q2.
q2 unlock -> q1.
q0 end -> .
q1 end -> .
%ENDA

Example 4

TRecS also supports a finite set of integers.

  _case n i e1 ... en

is reduced to ei, where i must range over {0,...,n-1}. See the example below.

%BEGING
S -> br (New (C 0)) (New (C 1)).
C b x -> F b x (G b x end).
F b x k -> _case 2 b k (Lock x k).  
G b x k -> _case 2 b k (Unlock x k).
New k -> br (newl (k I)) (k K).
I x y -> x y.
K x y -> y.
Lock x k -> x lock k.
Unlock x k -> x unlock k.
%ENDG
%BEGINA
q0 br -> q0 q0.
q1 br -> q1 q1.
q2 br -> q2 q2.
q0 newl -> q1.
q1 lock -> q2.
q2 unlock -> q1.
q0 end -> .
q1 end -> .
%ENDA