GTRecS (Games and 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 (non-deterministic) Buchi automata with a trivial acceptance condition. Note that on this web interface, only small examples can be tested (as the time-out is set to 3 seconds). Please contact Naoki Kobayashi if you need source code.

TRecS, another version of type-based model checker, is available here.


Reference

Naoki Kobayashi, A Practical Linear Time Algorithm for Trivial Automata Model Checking of Higher-Order Recursion Schemes, Proceedings of FoSSaCS 2011, LNCS 6604, pp.260-274, 2011

Examples

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

The following recursion scheme generates a tree representation of an infinite list [(0,1); (1,2); (2,3); ...]. The non-deterministic trivial automaton specifies the property that each pair in the list is either a pair of an even number and an odd number, or a pair of an odd number and an even number. 
%BEGING
S -> F Zero.
F x -> cons (P x) (F (Succ Zero)).
P x -> a (x s z) (Succ x s z).
Succ x s z -> s (x s z).
Zero s z -> z.
%ENDG

%BEGINA
q0 cons -> q1 q0.
q1 a -> qeven qodd.
q1 a -> qodd qeven.
qeven s -> qodd.
qodd s -> qeven.
qeven z -> .
%ENDA

Example 3

The following recursion scheme generates a huge tree, of the form a2225 c. The automaton describes the property that the number of "a" is even. 
%BEGING
S -> F0 G2 G1 G0.
F0 f x z -> F1 (F1 f) x z.
F1 f x z -> F2 (F2 f) x z.
F2 f x z -> F3 (F3 f) x z.
F3 f x z -> F4 (F4 f) x z.
F4 f x z -> F5 (F5 f) x z.
F5 f x z -> G3 f x z.
G3 f x z -> f (f x) z.
G2 f x -> f (f x).
G1 x -> a x.
G0 -> c.
%ENDG

%BEGINA
q0 a -> q1.
q1 a -> q0.
q0 c -> .
%ENDA

Example 4

An order-3 recursion scheme obtained from the resource usage verification problem for the following program: 
let rec f x y = if * then close x; close y 
                 else read x; write y; f x y in
let x = open_in "foo" in
let y = open_out "bar" in
   f x y
Here, the goal of verification is to check that "foo" is accessed according to read* close, and "bar" is accessed according to write* close. For the encoding, please consult our ICALP09 paper. 
%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 -> i x.
K x -> k x.
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.
qany br -> qany qany.
q0 newr -> qr.
q0 neww -> qw.
q0 k -> q0.
q0 read -> q0.
q0 write -> q0.
q0 close -> q0.
qr i -> qri.
qr k -> qrk.
qrk read -> qr.
qrk write -> qr.
qrk close -> qr.
qri read -> qr.
qri close -> qc.
qw i -> qwi.
qw k -> qwk.
qwk read -> qw.
qwk write -> qw.
qwk close -> qw.
qwi write -> qw.
qwi close -> qc.
qc k -> qck.
qck read -> qc.
qck write -> qc.
qck close -> qc.
qr newr -> qany.
qr neww -> qany.
qw newr -> qany.
qw neww -> qany.
qany i -> qany.
qany k -> qany.
qany read -> qany.
qany write -> qany.
qany close -> qany.
qany end -> .
qc end ->.
q0 end ->.
qrw end ->.
%ENDA