Restrictions

We summarize additional restrictions, bugs, and features in the current version of Maisie in the following:

1. Keywords: in addition to C, Maisie defined the following reserved words:
   • any word with prefix zz.
   • Other keywords:

     and at clocktype driver ename ename_cmp endsim entity etype hold invoke maxclock max message min msg mtype nnodes new or printmsg print_ename qempty qhead sclock self st timeout trace_msg trace until wait when with

2. The wait, hold, and trace statements may not be used within a function.
3. The mvar and ranker used in a resume condition can only be an identifier, in particular, they cannot be an array element or a field in a struct.