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