Lurch models begin with an optional C-code section, which is followed by two percent signs (%%) and then a list of finite-state machines; individual machines are separated by one or more blank lines. Each finite-state machine is a list of state declarations and / or transitions. Transitions may refer to the C-code section. For example, the model below represents a simple producer-consumer system:

enum { P, C } turn = P;

%%

pr_wait; (turn == P); -;           produce;
produce; -;           {turn = C;}; pr_wait;

cs_wait; (turn == C); -;           consume;
consume; -;           {turn = P;}; cs_wait;

The model begins with C; an enumerated type is used to declare the variable turn, which has two values: P and C. After the marker %% two finite-state machines are defined. The first machine, which represents a producer process, has two transitions (one on each line). The first says: when in the state pr_wait, if (turn == P) evaulates to true, it is possible to go to state produce. The dash in column three indicates that this transition has no output side effect. The second transitions says: from state produce it is possible to go directly to state pr_wait, and if the transition occurs {turn = C;} is executed as a side effect. Also, the first state listed in a machine is assumed by Lurch to be the initial state of the machine (pr_wait for the producer, cs_wait for the consumer).

To avoid conflicts with the C-code part of the model, Lurch global variables and function names begin with an underscore; main() also can not be used in the model. There are a few special functions called by Lurch at different times during its execution, all of which begin with an underscore:

void _before_all(void)	Called before Lurch's first attempt to find a path.
void _before(void)	Called before each of Lurch's attempts to find a path; can be used to set C variables to their initial values.
void _before_each(void)	Called before each step along a path.
void _score(void)	Called at the end of each time tick; can be used to modify a score value according to what Lurch reaches during that time tick.
void _after_each(void)	Called after each step along a path.
void _after(void)	Called after each attempt to find a path.
void _after_all(void)	Called after Lurch has finished looking for paths, or when the user hits CTRL-C to quit early.
void _hash(unsigned int *h)	Called each time Lurch calculates a hash value for a global state; can be used to include C variable values in the calculation, so that two otherwise identical states with different C variable values are treated as different states (*h comes in as the value of the global state hash; it can be modified by this function).
void _print(char *c)	Called each time a global state is output to a counter example trace file; can be used to include C variable information in the trace file. The constant _MAX_PRINT can be set to accommodate whatever length string is needed for this information.
void _tr_incr(_Tran *tr)	Called after each transition processed by Lurch; can be used to track information about how many times particular transitions are executed by Lurch.

In the finite-state machine part of the model, machines are described by lists of mutually exclusive states and transitions. States may be declared alone, but if they are included as the start or next state of a transition they do not need to be declared separately. The model below shows two machines declared as sets of states (three each) and two declared as sets of transitions, with their states implied:

%%

f1t.
f1p;
f1n;

f2t.
f2p;
f2n;

p1w; f1t; f1p;     p1l;
p1w; f2t; f2n;     p1r;
p1l; f2t; f2n;     p1e;
p1r; f1t; f1p;     p1e;
p1e; -;   f1t,f2t; p1w.

p2w; f2t; f2p;     p2l;
p2w; f1t; f1n;     p2r;
p2l; f1t; f1n;     p2e;
p2r; f2t; f2p;     p2e;
p2e; -;   f2t,f1t; p2w.

In this model the C-code section is empty. Also, certain local states are followed by a period instead of a semicolon. This is to indicate that they are legal end states. When Lurch searches for a deadlock (as in this model, which represents the dining philosophers problem for two philosophers sharing two forks), Lurch must know, for each machine, which of its local states are legal end states. If Lurch reaches the end of a path and one or more machines is not in a legal end state, a deadlock is reported. This model also shows how transition columns 2 and 3, the input and output columns, may refer not just to the C-code section but also to other finite-state machines. A transition which includes, as an input condition, a state from some other machine, can only be executed if that machine is in that state. And if a transition with a state from another machine in its output column is executed, it sets that machine to that state as a side effect. For example, the transition p2w; f2t; f2p; p2l; can proceed if its machine is in state p2w and the second machine is in state f2t (philosopher two is waiting and fork two is on the table). If it does proceed it sets the second machine to state f2p and sets its own machine to state p2l (fork two is in the hand of the previous philosopher, i.e., philosopher two, and philosopher two has a fork in his left hand).

In addition to using periods vs. semicolons to mark legal end states, there are a few other special marks recognized by Lurch in finite-state machine definitions:

_fault	Local states beginning with an underscore are considered faults. For example, a transition representing an assertion violation would lead to a fault state; if Lurch found a path to the violation this transition would be executed, and when the fault state was reached it would be reported.
#progress	The SPIN model checker is capable of finding "no-progress" cycles present in a system. These are global state cycles in which no local state marked as representing progress is reached. Lurch can also find these cycles, and when doing so assumes that any local state beginning with a pound sign represents progress (note: in older version of Lurch, progress states were marked with a plus sign, but this caused problems for the parser in the current protype GUI version).
=accept	The SPIN model checker uses Büchi automata to represent negated temporal logic properties in "never" clauses. By definition, a Büchi automata accepts an input that causes it to continue in a cycle that includes an accept state (as opposed to a normal finite-state machine, which accepts an input that causes it to stop in its accept state). In order to find acceptance cycles, Lurch needs to know which states in a machine representing a Büchi automaton are accept states; their names must begin with an equals sign.