Allow fluents directly in controllerSpec assumption and liveness (not only assertion names)
Title: Allow fluents directly in controllerSpec assumption and liveness (not only assertion names)
Description: Currently assumption = {…} and liveness = {…} in a controllerSpec take assertion names — each must be a previously declared assert NAME = . Requesting that these clauses also accept fluents directly (and, ideally, inline boolean fluent formulae), so users don't have to wrap every fluent in a named assert.
Current (works): fluent FG = <g, {a,b,c,d,e,f}> assert G = FG controllerSpec Spec = { assumption = {G} liveness = {E, D} controllable = {a, c, e} }
Desired: fluent FG = <g, {a,b,c,d,e,f}> controllerSpec Spec = { assumption = {FG} // fluent used directly liveness = {FE, FD} // fluents used directly controllable = {a, c, e} }