The main changes in the UCLID models for using UCLID_PA tool are in the CONTROL section of the file. The main sub-sections under the CONTROL section are:
CONTROL

EXTVAR (* just legacy sections, never used *)

STOREVAR (* just legacy sections, never used *)

VAR (* just legacy sections, never used *)

CONST (* declaring constant Booleans, terms, functions, predicates *)
a : TERM ;
b : TERM ;
x : TERM ;

DEFINE (* define some macros here *)

AXIOMS (* specify universally quantified axioms here *)

(* These axioms are asserted while doing predicate abstraction
* or for checking validity
*)

(* important axiom about the max *)
ax1 := FORALL (x) b.max > b.number(x) ;

(* axioms assume a quantified expression *)
ax2 := FORALL (x) b.NPROCS > b.ZERO ;



PREDICATES (* new section for specifying predicates *)

QUANTVARS (* specify the set of index variables/terms *)
i1 : TERM ;
i2 : TERM ;

QUANTPREDS (* specify the indexed predicates *)

(* some examples provided here *)
(* there predicates are expressions over the state variables
and the index variables specified in QUANTVARS section
*)


p1:= (b.pc(i1)=L0) ;

p2 := (i1<b.ZERO) ;

p3 := (b.number(i1)<b.number(i2)) ;

p4 := (i2=i1) ;


SPEC (* specify the safety property to be proved *)
(a!=b) => ~(b.pc(a) = L5 & b.pc(b) = L5) ;

EXEC (* legacy section, never used *)




For performing predicate discovery, we sometime specify the variables which should not appear in the predicates. These are explicitly declared as "INPUTVAR" in a given module. The INPUTVAR section appears between the VAR and the CONST section in a given module. The following example shows a case, where the variables "pid", "max" and "arb" are declared as INPUTVAR, so that they do not appear in the predicates.

VAR
(********* state variables **************)

(* components of each process *)
pc : FUNC[1] of LOC;
choosing : PRED[1];
number : FUNC[1];
j : FUNC[1] ;
max : TERM ;
pid : TERM ; (* making pid a state variable, so that
one only sees pid in the next state expr *)

(********* arbitrary value generator *****)
arb : TERM ;

INPUTVAR
(* these are not included in predicates during predicate generation *)
pid : TERM ;
max : TERM ;
arb : TERM ;

CONST