set_trans :  (string * Term.term) list -> model -> model
STRUCTURE
holCheckLib
SYNOPSIS
Sets the transition system for a HolCheck model.
DESCRIPTION
The transition system is supplied as list of (transition label, transition relation) pairs. Each label must be a unique string. Each relation must be a propositional term, in which primed variables represent values in the next state. The transition label "." is internally used as a wildcard that is expected to match all transitions, and is thus not allowed as a transition label, unless there is only one transition.
FAILURE
Fails if the transition labels are not unique, or the transition list is empty, or the wildcard label is used with a non-singleton transition list, or any of the relation terms is not a quantified boolean formula (QBF).
EXAMPLE
For a mod-8 counter, we need three boolean variables to encode the state. The single transition relation can then be set as follows (assuming holCheckLib has been loaded): 

- val m = holCheckLib.set_trans [("v0", ``v0' = ~v0``), ("v1", ``v1' = (v0 \/ v1) /\ ~(v0 = v1)``),
	             ("v2", ``v2' = (v0 /\ v1 \/ v2) /\ ~(v0 /\ v1 = v2)``)] holCheckLib.empty_model;
> val m = <model> : model

where empty_model can be replaced by whatever model the user is building.

COMMENTS
This information must be set for a HolCheck model.
SEEALSO
holCheck, empty_model, get_trans, set_flag_ric
HOL  Kananaskis-10