These are arguments of module calls that can be optional since wildcards can be used in the Quartz language.

a Generic consists of a loop variable and its lower and upper bounds

LineNr is used as abbreviation of those integers that denote the line numbers from which the statement has been parsed.

The type checker function Uty2Stmt produces a struct TypeInfo with the following attributes:

• msgs is a list of messages that is empty if the type-checking was successful, and contains otherwise messages to report the type errors.
• lblL is the list of control flow labels in the typed statement (note that new labels can be generated due to unrolling of generic statements).
• lcVL contains the declarations of the declared local variables (note again that new local variables may be generated by unroling of generic statements).
• lcNL contains the names of assertions, assumptions etc.
• orcL contains the declarations of introduced oracle variables used to replace nondeterministic statements.
• stmt finally is the generated typed statement.

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.

UtyDeclStmt is the untyped version of DeclStmt; it contains:

• name which is the index of the name of the UtyDeclStmt (in the Nametable)
• decL is the list of interface variable declarations (inputs, outputs, inouts)
• stmt is an untyped statement

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.

untyped Quartz modules consist of the following entries (some of them refer to the file from which the module has been read from):

• quartzFileDir is the name of the file's (absolute path) directory
• quartzFileName is the name of the Quartz file without suffix ".qrz"
• rootDir specifies the root directory to which the import paths refer to
• importPaths determines the directories where called modules are searched; these directories are {rootDir+i { i in importPaths} }
• macros is a map that stores macro definitions of a Quartz file. It maps the name of the macro function to a pair (xL,tau) where xL is the list of formal arguments and tau the right-hand side of the macro definition. For example, the macro definition "max(a,b) = ((a>b)?a:b)" maps the name "max" to the pair ([a,b],((a>b)?a:b)).
• utyDeclStmt is an untyped statement with the name of the untyped module, its declarations, and its untyped body statement
• obsrvSpecL is the list of specifications that may be endowed with observers
• driverL is the list of drivers that can be used to generate closed systems for simulation

This data type implements untyped statements as generated by the parser. Each untyped statement stores also the line number where it has been parsed from for means of error reporting (if the type-checking should fail). In addition to the typical statements that also appear as Quartz statements, there some further statements that are eliminated by the type-checker:

• UtyNothing,UtyAction,UtyPause,UtyConditional,UtySequence,UtyDoWhile, and UtyWhileDo should be self-explaining.
• UtySyncParAnd(ln,S1,S2) is a synchronuous parallel execution of S1 and S2 that is active if both S1 and S2 are active.
• UtySyncParOr(ln,S1,S2) is a synchronuous parallel execution of S1 and S2 that is active if at least one of S1 and S2 is active.
• UtySuspend,UtySuspendW,UtySuspendI,UtySuspendWI are suspension statements, where weak and immediate variants are suffixed by W and I, respectively.
• UtyAbort,UtyAbortW,UtyAbortI,UtyAbortWI are abortion statements, where weak and immediate variants are suffixed by W and I, respectively.
• UtyDuring,UtyDuringF,UtyDuringI,UtyDuringIF are the four variants of during statement. Note that during(S1,S2) executes the instantaneous statement S2 in each macro step where S1 executes. The four variants differ in that they include the initial and final steps also indicated by the I and F suffixes.
• UtyLetDec(ln,[(x1,e1);...;(xN,eN)],S) declares local variables xi that are identified with expressions ei in the statement S.
• UtyLocDec(ln,[(x1,d1);...;(xN,dN)],S) declares local variables xi having declaration di for statement S.
• UtyModuleCall(ln,i,m,argL) is a module call to module m with argument list argL, and the name of this call is i (i and m are indices of the NameTable).
• UtyContFlow(ln,w1,w2,S,sigma) is a flow statement to define the continuous evolution of a hybrid system via the actions in S until the condition sigma holds (which terminates the continuous phase).
• UtyGen* are generic statements that are given a triple (ln,generic,S), where generic is a tuple (xn,min,max). The meaning is that first instances [Smin;...;Smax] are generated by replacing variable xn in S by the nat constants min;...;max, and these statements are combined as a sequence, synchronous parallel, etc. according to the operator.
• UtyCaseStmt(ln,[(b1,S1);...;(bN,SN)],S) represents a case statement that executes Si when bi holds, and S if none of the Si holds. It only executes the first Si whose bi is true.
• UtyAsyncParOr(ln,S1,S2) implements an asynchronous parallel execution that executes either one step of S1, or one step of S2 or steps of both S1 and S2 in common. The statement is active as long as one of the two statements is active.
• UtyAsyncParAnd(ln,S1,S2) implements an asynchronous parallel execution that executes either one step of S1, or one step of S2 or steps of both S1 and S2 in common. The statement is active as long as both of the two statements are active.
• UtyInterleaveOr(ln,S1,S2) implements an interleaved parallel execution that executes either one step of S1 or one step of S2. The statement is active as long as one of the two statements are active.
• UtyInterleaveAnd(ln,S1,S2) implements an interleaved parallel execution that executes either one step of S1 or one step of S2. The statement is active as long as both of the two statements are active.
• UtyChoice(ln,S1,S2) nondeterministically (and dynamically) chooses that executes Si when bi holds, and S if none of the Si holds. It only between S1 and S2.
• UtyGenContFlow(ln,rl,cl,actL,sigma) is a generic flow statement with action list actL and optional release condition sigma. Note that only the action list is unrolled, and packed into a flow statement having the same rl,cl, and sigma.
• UtyHalt is Esterel's halt statement.
• UtyLoop(ln,S) infinitely often repeats the execution of S.
• UtyLoopEach and UtyEveryDo are Esterel's loop S each(b) and every-loop.
• UtyAwait and UtyAwaitI are the await statements that stop the control and wait until the given condition holds. The immediate form is UtyAwaitI. Both statements therefore define a new control flow location.
• UtyAlways(ln,qn,S) abbreviates UtyLoop(ln,UtySequence(ln,UtyPause(ln,qn),S))
• UtyAlwaysI(ln,qn,S) abbreviates UtyLoop(ln,UtySequence(ln,S,UtyPause(ln,qn)))