Named state sets, so a spec can refer to a whole set (e.g. old(phase(this))) #435

Motivation

Each @StateSet becomes an anonymous ghost function (state1, state2, ...). After a call, AuxStateHandler.getMissingStates adds stateN(this) == stateN(old(this)) for every set the to predicate does not mention, so unmentioned sets keep their value. That works, but the spec author cannot name a set, which causes three problems.

Running example: an UndoManager spec with three orthogonal sets. The phase decides addEdit/setLimit; whether there is something to undo or redo decides undo()/redo(), and canUndo()/canRedo() are guards.

@StateSet({"start", "canEdit", "end"})
@StateSet({"undoable", "notUndoable"})
@StateSet({"redoable", "notRedoable"})
...
@StateRefinement(from="undoable(this)", to="notUndoable(this) && redoable(this)")
void undo();

@StateRefinement(from="undoable(this)", to="return && undoable(this)")
@StateRefinement(to="return ? undoable(this) : notUndoable(this)")
boolean canUndo();

1. A set mentioned in one branch is dropped in the other

A set counts as "mentioned" if any of its states appears anywhere in to. With to="return ? undoable(this) : true", the undo set is not carried over in the false branch: it becomes unconstrained instead of keeping its previous value. Verified with verifier 0.0.36 (addEdit; boolean b = um.canUndo(); um.undo();). The found predicate carries state1(um⁸⁵) == state1(um⁸³) && state3(um⁸⁵) == state3(um⁸³) but has no equality for state2. There is no way to write "in this branch, keep the set as it was".

2. Error messages leak the internal names

State Refinement Error: found canEdit(um⁸³) && undoable(um⁸³) && notRedoable(um⁸³) && (canUndo⁸⁴ ? undoable(um⁸⁵) : notUndoable(um⁸⁵)) && state1(um⁸⁵) == state1(um⁸³) && state3(um⁸⁵) == state3(um⁸³) but expected undoable(um⁸⁵)

state1 and state3 appear nowhere in the spec.

3. Hints multiply all sets together

For an unknown receiver (a field or a getter result), the hint lists the cross product of all sets, although the failing call only needs one:

The state of undoManager is unknown here. To get it to start and undoable and redoable or start and notUndoable and redoable or canEdit and undoable and redoable or canEdit and notUndoable and redoable or end and undoable and redoable or end and notUndoable and redoable, use: undoManager.undo() (from start and undoable and notRedoable or canEdit and undoable and notRedoable or end and undoable and notRedoable)

redo() only needs redoable. A hint per named set could say "undoManager is not known to be redoable; check canRedo()". The guard canRedo() is missing from the hint entirely, because it is a from-less refinement whose result decides the state (related: liquid-java/liquidjava-fsm#14).

Proposal

Allow an optional name on a state set, which can be used as a function in predicates:

@StateSet(name="phase", value={"start", "canEdit", "end"})
@StateSet(name="undo",  value={"undoable", "notUndoable"})
@StateSet(name="redo",  value={"redoable", "notRedoable"})

@StateRefinement(to="return ? undoable(this) : undo(this) == old(undo(this))")
boolean canUndo();

• undo(this) == old(undo(this)) keeps a set explicitly, per branch (fixes 1).
• Messages print phase(um) / undo(um) instead of state1(um) (fixes 2).
• Hints can name only the set the failing precondition needs (helps 3).
• Return one machine per @StateSet liquidjava-fsm#8 ("one machine per @stateset") could use the names as machine titles.

Unnamed sets would keep working as today, with the generated name.

Context: found while writing UndoManager specs for LiquidJava study exercises (JabRef's EditAction, where undo()/redo() on a manager from a getter must be guarded by canUndo()/canRedo()).