% Vagrant robot from Henzinger Hoi 1994 % BEGIN FIXED PREAMBLE :- multifile r/5, var2names/2, preds/2, cube_size/1, start/1, refinement/1, error/1. refinement(inter). cube_size(1). % END FIXED PREAMBLE /* ARMC uses logical variables to model system variables. In Prolog, logical variables start with either capital letter or underscore. Control locations and transition ids are represented by Prolog terms. For more information about Prolog variables and terms see: http://www.sics.se/sicstus/docs/latest/html/sicstus.html/ ARMC uses the assertions of CLP(Q, R) to represent transition relations, see: http://www.sics.se/sicstus/docs/latest/html/sicstus.html/Solver-Predicates.html#Solver-Predicates */ start(pc(start)). % Define the initial location error(pc(error)). % Define the error location /* Define mapping between logical variables, which represent variables of the analyzed system, and the corresponding system variables. */ var2names(p(_, data(X, Y, T)), [(X, 'x'), (Y, 'y'), (T, 't')]). /* Define initial set of predicates, e.g. [X+Y>=T]. Empty list [] corresponds to the empty set. */ preds(p(_, data(X, Y, T)), []). /* Defines a transition */ r(p( pc(start), % from-location of the transition data(X, Y, T) % variables at the from-location ), p( pc(l0), % to-location of the transtion data(X1, Y1, T1) % variables at the to-location (`primed' variables) ), [X1=0, Y1=0, T1=0], % transition relation given by an assertion over from- and to-variables [], % empty list, used for modeling C-programs 0). % unique transition id r(p(pc(l0), data(X, Y, T)), p(pc(l1), data(X1, Y1, T1)), [T1-T=