GitLab

So, it turns out that when we reference a parametrised fluent (e.g. fluent Fail in the example below) with no parameter (i.e. bad reference) the tool assumed the referenced fluent is, in fact, an event fluent (for the "Fail" event). Hence, it produces a fluent for the event that was in fact the name of the parametrised fluent (i.e. Fail). See example below for details. The code where the sin occurs is in FluentTransformerVisitor line 145 code:

// the predicate definition is an event. Create a fluent. if (predicateDefinition == null){ Fluent resultantFluent = generateFluentFromEvent(name); this.actionFluentsForUpdate.add(resultantFluent); return resultantFluent; }

The fsp example showing this bug is:

const Zise = 4 range R = 0..Zise

set ControllableActions = {idle} set UncontrollableActions = {action} set Alphabet = {ControllableActions, UncontrollableActions}

ENV = (action->ENV).

fluent Fail[var:R] = < {anAction[var]}, Alphabet{anAction[var]}> assert Failures = Fail constraint CFailures = Failures ||TEST = CFailures.

controllerSpec SPEC = { failure = {Failures} controllable = {ControllableActions} }

controller ||C = (ENV)~{SPEC}. ||ANIMATE = (C || ENV).