UtyAction is the data type for untyped actons that are generated by the parser for type-checking. There are two categories of actions:

• discrete actions:
• UtyAssignNow(lhs,rhs) represents an immediate assignment lhs := rhs.
• UtyAssignNxt(lhs,rhs) represents a delayed assignment next(lhs) := rhs.
• UtyAssert(qn,sigma) demands that sigma must hold here, and qn is the name of this assertion.
• UtyAssume(qn,sigma) assumes that sigma holds here, and qn is the name of this assumption.
• continuous actions (for modeling hybrid systems):
• UtyAssignFlw(lhs,rhs) represents a flow assignment lhs := rhs that hold during a continuous transition.
• UtyAssignDrv(lhs,rhs) represents a derivation flow assignment der(lhs) := rhs to assert that rhs is the derivation of lhs.
• UtyConstrain(qn,BND,sigma) demands that sigma holds during the continuous transition where this action is executed (BND is determines the validity on the bounds of the interval).
• UtyReleaseMay(qn,sigma) describes when a continuous transition will terminate.