Spin Version 3.0: Language Reference

• Concise Reference
• Semantics model
• Promela grammar
• MetaTerms:
  comments, false, inline, ltl, macros, skip, true,
• Declarators:
  accept, active, arrays, chan, datatypes, end, hidden, init, mtype, never, notrace, priority, proctype, progress, provided, show, trace, typedef, xr, xs,
• ControlFlow:
  atomic, break, d_step, do, goto, if, labels, separators, sequence, unless,
• BasicStatements:
  assert, assign, condition, printf, receive, send,
• Predefined:
  _, _last, _pid, cond_expr, else, empty, enabled, eval, full, len, nempty, nfull, np_, pc_value, poll, remoterefs, run, timeout,
• Omissions:
  float, hierarchy, pointers, probabilities, procedures, rand, realtime, scanf,