mod ICASE1 {
  pr(ISTEP)
-- arbitrary objects
  op p10 : -> Process .
-- assumptions
  -- eq c-begin(s,p10) = true .
  eq pc(s,p10) = l1 .
  eq locked(s) = false .
-- successor state
  eq s' = begin(s,p10) .
}

mod ICASE2 {
  pr(ISTEP)
-- arbitrary objects
  op p10 : -> Process .
-- assumptions
  -- eq c-exit(s,p10) = false .
  eq pc(s,p10) = cs .
-- successor state
  eq s' = exit(s,p10) .
}

mod ICASE3 {
  pr(ISTEP)
-- arbitrary objects
  op p10 : -> Process .
-- assumptions
  -- eq c-end(s,p10) = false .
  eq pc(s,p10) = l2 .
-- successor state
  eq s' = end(s,p10) .
}