HorSat2: A model checker for HORS based on SATuration

This is a Web interface for HorSat2: a saturation-based model checker for higher-order recursion schemes (HORS). HorSat2 is based on

Christopher Broadbent and Naoki Kobayashi, Saturation-Based Model Checking of Higher-Order Recursion Schemes,

but a number of changes/optimizations (in particular, in the treatment of flow information) have been applied, as partially described in:

Naoki Kobayashi, HorSat2: A Saturation-Based Higher-Order Model Checker, a draft tool paper, 2016,

Enter a HORS and a tree automaton (in the TRecS format) in the box below, choose an option, and press the "submit" button. The property should be given either in the form of a trivial deterministic tree automaton (a top-down deterministic tree automaton with trivial acceptance conditions) or a trivial alternating tree automaton. Some examples are given below. More examples are available here and here as zip files. Note that on this web interface, only small examples can be tested (as the time-out is set to 3 seconds). The source code is available here.

Examples

Some examples are given below.

Example 1

%BEGING    /*** Rewring rules of a HORS. 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 1'

The same grammar and property as above, but the automaton is written in the style of topdown alternating tree automaton.

%BEGING    
S -> F c.  
F x -> a x (F (b x)).  
%ENDG

%BEGINR   /* arity of each tree constructor */
a -> 2.
b -> 1.
c -> 0.
%ENDR

%BEGINATA /* alternating transition rules */
q0 a -> (1,q0) /\ (2,q0).
q1 a -> false.
q0 b -> (1,q1).
q1 b -> (1,q1).
q0 c -> true.
q1 c -> true.
%ENDATA

Example 2

The following HORS generates a huge tree, of the form a^{2^{2^2⁵}} 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 3

/*** 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