There are two kinds of UtyProofGoals:

• UtySpecAssume(qn,sigma) declares an assumption with name qn and condition sigma that can be a temporal logic path formula.
• UtySpecAssert(qn,task,CL,phi,AL) declares an assertion with name qn and condition phi that can be a temporal logic path formula. The assumptions whose names are listed in AL are added as premises for the assertion, and if AL should be empty all known assumptions of the module are added. Moreover, the variables whose names are listed in CL are viewed as controllable, so that the problem is a model checking problem when CL is not empty, and otherwise, we have a controllability problem.