Quantifiers `forall`/`exists` cannot be used with labels in SPEC

[alexandertepaev]

R-CHECK currently rejects specifications where quantified formulas (forall, exists) refer to statement labels.
For example:

agent TestAgent
  local:
    done: bool
  init: !done
  repeat:
  (
    s1: {!done} *! (false)()[done := true]
  )

system = TestAgent(a1, true) || TestAgent(a2, true)

SPEC a1-s1 -> X a1-done
SPEC a2-s1 -> X a2-done
SPEC forall a : TestAgent . F a-done
SPEC forall a : TestAgent . a-s1 -> X a-done // <<< does not work

nuxmv returns following error:

Command failed: nuxmv -source /tmp/ltlspec-1KmPNLH/file.smv /tmp/file5182856115839989193.smv WARNING: single-value variable 'a1-automaton-state' has been stored as a constant WARNING: single-value variable 'a2-automaton-state' has been stored as a constant TYPE ERROR file /tmp/file5182856115839989193.smv: line 63 : undefined identifier 'a-s1' TYPE ERROR file /tmp/file5182856115839989193.smv: line 63 : undefined identifier 'a-s1' ERROR: Property "((!a-s1 | X a2-done) & (!a-s1 | X a1-done)) �" is not correct or not well typed. aborting 'source /tmp/ltlspec-1KmPNLH/file.smv'

Looks like labels are interpreted directly without being bound to a particular agent instance.