[tulip-control-users] Qinit in GRSpec question

[Joshua S. <jsh...@te...>]

Are there any further examples or sources for using the quantification
option associated with GRSpec besides the descriptions provided in the
documentation examples (which all appear to just use \E \A)?

Specifically I'm trying to better understand the warning messages,
"WARNING: `qinit = "\A \A"` but not `EnvInit => SysInit`" and "WARNING:
`qinit = '\A \A'` but not `EnvInit => (\E y': SysNext)`"

Joshua
-------------- next part --------------
An HTML attachment was scrubbed...