A status is one of "failed", "delayed", "success".
A mission is one of "offensive", "defensive".
A launch is one of "single", "double".
It is prohibited that
a mission M employs launch "double" and also
mission M has_state status S and also
status S is different from status "failed".
The last rule compiles to the following with the online tool:
Consider the following example:
The last rule compiles to the following with the online tool:
Shouldn't the literal
different_from(S, "failed")
beS != "failed"
instead?The same pattern holds if instead of using quoted-strings as object constants I use just elementary symbols (i.e., instead of
"failed"
I usefailed
).