diff --git a/liquidjava-example/src/main/java/testSuite/ErrorStateHintConstructors.java b/liquidjava-example/src/main/java/testSuite/ErrorStateHintConstructors.java new file mode 100644 index 00000000..f1487c62 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/ErrorStateHintConstructors.java @@ -0,0 +1,55 @@ +package testSuite; + +import liquidjava.specification.StateRefinement; +import liquidjava.specification.StateSet; + +// Each constructor creates the needed state, but only one that can be called is suggested +@StateSet({"fresh", "ready"}) +public class ErrorStateHintConstructors { + + @StateRefinement(to = "ready(this)") + public ErrorStateHintConstructors() {} + + @StateRefinement(from = "ready(this)", to = "fresh(this)") + public void use() {} + + // a concrete class: the constructor is suggested + static void concrete(ErrorStateHintConstructors value) { + value.use(); // Expect: State Refinement Error + } + + // the receiver is this object, which a new object would not change + public void self() { + this.use(); // Expect: State Refinement Error + } +} + +@StateSet({"fresh", "ready"}) +abstract class ErrorStateHintConstructorsAbstract { + + @StateRefinement(to = "ready(this)") + public ErrorStateHintConstructorsAbstract() {} + + @StateRefinement(from = "ready(this)", to = "fresh(this)") + public void use() {} + + static void fail(ErrorStateHintConstructorsAbstract value) { + value.use(); // Expect: State Refinement Error + } +} + +@StateSet({"fresh", "ready"}) +class ErrorStateHintConstructorsPrivate { + + @StateRefinement(to = "ready(this)") + private ErrorStateHintConstructorsPrivate() {} + + @StateRefinement(from = "ready(this)", to = "fresh(this)") + public void use() {} +} + +class ErrorStateHintConstructorsPrivateUser { + static void fail(ErrorStateHintConstructorsPrivate value) { + value.use(); // Expect: State Refinement Error + } +} diff --git a/liquidjava-example/src/main/java/testSuite/ErrorStateHintJoins.java b/liquidjava-example/src/main/java/testSuite/ErrorStateHintJoins.java new file mode 100644 index 00000000..7ea7f352 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/ErrorStateHintJoins.java @@ -0,0 +1,40 @@ +package testSuite; + +import liquidjava.specification.StateRefinement; +import liquidjava.specification.StateSet; + +// Joins of the states reached on different paths are not a lack of knowledge +@StateSet({"closed", "opened"}) +@StateSet({"unlocked", "locked"}) +public class ErrorStateHintJoins { + + @StateRefinement(to = "closed(this) && unlocked(this)") + public ErrorStateHintJoins() {} + + @StateRefinement(from = "closed(this)", to = "opened(this)") + public void open() {} + + @StateRefinement(from = "unlocked(this)", to = "locked(this)") + public void lock() {} + + @StateRefinement(from = "closed(this) && unlocked(this)") + public void enter() {} + + // every combination of the two state sets is reached on some path + public static void everyState(boolean p, boolean q) { + ErrorStateHintJoins d = new ErrorStateHintJoins(); + if (p) + d.open(); + if (q) + d.lock(); + d.enter(); // Expect: State Refinement Error + } + + // the paths differ in one of the two state sets the call checks, so both states are named in full + public static void oneSet(boolean p) { + ErrorStateHintJoins d = new ErrorStateHintJoins(); + if (p) + d.open(); + d.enter(); // Expect: State Refinement Error + } +} diff --git a/liquidjava-example/src/main/java/testSuite/ErrorStateHintNaming.java b/liquidjava-example/src/main/java/testSuite/ErrorStateHintNaming.java new file mode 100644 index 00000000..c91896ed --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/ErrorStateHintNaming.java @@ -0,0 +1,59 @@ +package testSuite; + +import liquidjava.specification.StateRefinement; +import liquidjava.specification.StateSet; + +// The needed and current states are named only in the state sets that matter +@StateSet({"created", "open", "ready"}) +@StateSet({"quiet", "loud"}) +public class ErrorStateHintNaming { + + @StateRefinement(to = "created(this) && quiet(this)") + public ErrorStateHintNaming() {} + + // a state of either set: each is named alone, not combined with every state of the other set + @StateRefinement(from = "open(this) || loud(this)") + public void read() {} + + public static void use(ErrorStateHintNaming s) { + s.read(); // Expect: State Refinement Error + } +} + +// every state allows flip(), each by its own refinement: a or b, not all six states +@StateSet({"a", "b"}) +@StateSet({"x", "y", "z"}) +class ErrorStateHintNamingToggle { + + @StateRefinement(to = "a(this) && x(this)") + public ErrorStateHintNamingToggle() {} + + @StateRefinement(from = "a(this)", to = "b(this)") + @StateRefinement(from = "b(this)", to = "a(this)") + public void flip() {} + + public static void use(ErrorStateHintNamingToggle t) { + t.flip(); // Expect: State Refinement Error + } +} + +// known in one of three state sets: only that set is named +@StateSet({"start", "canEdit", "end"}) +@StateSet({"undoable", "notUndoable"}) +@StateSet({"redoable", "notRedoable"}) +class ErrorStateHintNamingPartlyKnown { + + @StateRefinement(to = "start(this) && notUndoable(this) && notRedoable(this)") + public ErrorStateHintNamingPartlyKnown() {} + + @StateRefinement(from = "redoable(this)", to = "undoable(this) && notRedoable(this)") + public void redo() {} + + @StateRefinement(from = "undoable(this)", to = "notUndoable(this) && redoable(this)") + public void undo() {} + + @StateRefinement(from = "notRedoable(this)") + public void check() { + this.redo(); // Expect: State Refinement Error + } +} diff --git a/liquidjava-example/src/main/java/testSuite/ErrorStateHintUnknownAnyState.java b/liquidjava-example/src/main/java/testSuite/ErrorStateHintUnknownAnyState.java new file mode 100644 index 00000000..07bf3c46 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/ErrorStateHintUnknownAnyState.java @@ -0,0 +1,28 @@ +package testSuite; + +import liquidjava.specification.StateRefinement; +import liquidjava.specification.StateSet; + +// reset() works in any state, so it is suggested even though the state is unknown; open() alone is not +@StateSet({"created", "open", "closed"}) +public class ErrorStateHintUnknownAnyState { + + @StateRefinement(to = "created(this)") + public ErrorStateHintUnknownAnyState() {} + + @StateRefinement(to = "created(this)") + public void reset() {} + + @StateRefinement(from = "created(this)", to = "open(this)") + public void open() {} + + @StateRefinement(from = "open(this)") + public void read() {} + + @StateRefinement(from = "open(this)", to = "closed(this)") + public void close() {} + + public static void use(ErrorStateHintUnknownAnyState f) { + f.read(); // Expect: State Refinement Error + } +} diff --git a/liquidjava-example/src/main/java/testSuite/classes/state_hint_checked_error/Reader.java b/liquidjava-example/src/main/java/testSuite/classes/state_hint_checked_error/Reader.java new file mode 100644 index 00000000..1477fa12 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/classes/state_hint_checked_error/Reader.java @@ -0,0 +1,26 @@ +package testSuite.classes.state_hint_checked_error; + +import java.util.Scanner; + +// A failed check of the receiver does not decide its state; a check of another object says nothing about it +public class Reader { + + public static void failedCheck(Scanner it) { + if (!it.hasNext()) { + it.next(); // Expect: State Refinement Error + } + } + + public static void failedCheckOfTheSameScanner(Scanner scanner) { + Scanner same = scanner; + if (!scanner.hasNext()) { + same.next(); // Expect: State Refinement Error + } + } + + public static void checkOfAnotherScanner(Scanner other, Scanner input) { + if (other.hasNext()) { + input.next(); // Expect: State Refinement Error + } + } +} diff --git a/liquidjava-example/src/main/java/testSuite/classes/state_hint_checked_error/ScannerRefinements.java b/liquidjava-example/src/main/java/testSuite/classes/state_hint_checked_error/ScannerRefinements.java new file mode 100644 index 00000000..3f39486d --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/classes/state_hint_checked_error/ScannerRefinements.java @@ -0,0 +1,17 @@ +package testSuite.classes.state_hint_checked_error; + +import liquidjava.specification.ExternalRefinementsFor; +import liquidjava.specification.Refinement; +import liquidjava.specification.StateRefinement; +import liquidjava.specification.StateSet; + +@StateSet({"hasMore", "noMore"}) +@ExternalRefinementsFor("java.util.Scanner") +public interface ScannerRefinements { + + @Refinement("_ == true --> hasMore(this)") + boolean hasNext(); + + @StateRefinement(from = "hasMore(this)", to = "noMore(this)") + String next(); +} diff --git a/liquidjava-example/src/main/java/testSuite/classes/state_hint_undo_manager_error/Editor.java b/liquidjava-example/src/main/java/testSuite/classes/state_hint_undo_manager_error/Editor.java new file mode 100644 index 00000000..05c5c612 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/classes/state_hint_undo_manager_error/Editor.java @@ -0,0 +1,15 @@ +package testSuite.classes.state_hint_undo_manager_error; + +import javax.swing.undo.UndoManager; + +public class Editor { + + static UndoManager history() { + return new UndoManager(); + } + + static void redoLast() { + UndoManager undoManager = history(); + undoManager.redo(); // Expect: State Refinement Error + } +} diff --git a/liquidjava-example/src/main/java/testSuite/classes/state_hint_undo_manager_error/UndoManagerRefinements.java b/liquidjava-example/src/main/java/testSuite/classes/state_hint_undo_manager_error/UndoManagerRefinements.java new file mode 100644 index 00000000..8bee5cd1 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/classes/state_hint_undo_manager_error/UndoManagerRefinements.java @@ -0,0 +1,26 @@ +package testSuite.classes.state_hint_undo_manager_error; + +import liquidjava.specification.ExternalRefinementsFor; +import liquidjava.specification.StateRefinement; +import liquidjava.specification.StateSet; + +// Issue #454: with an unknown state, redo() needs redoable, and the only call that leads there, undo(), needs +// undoable, which is just as unknown +@ExternalRefinementsFor("javax.swing.undo.UndoManager") +@StateSet({"undoable", "notUndoable"}) +@StateSet({"redoable", "notRedoable"}) +public interface UndoManagerRefinements { + + @StateRefinement(to = "notUndoable(this) && notRedoable(this)") + void UndoManager(); + + @StateRefinement(from = "redoable(this)", to = "undoable(this) && notRedoable(this)") + void redo(); + + @StateRefinement(from = "undoable(this)", to = "notUndoable(this) && redoable(this)") + void undo(); + + @StateRefinement(from = "redoable(this)", to = "return && redoable(this)") + @StateRefinement(to = "return ? redoable(this) : notRedoable(this)") + boolean canRedo(); +} diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/hints/Hint.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/hints/Hint.java index bb6834dc..4ce0e7ac 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/hints/Hint.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/hints/Hint.java @@ -25,8 +25,8 @@ public enum Kind { PATH_DEPENDENT_STATE, /** The object is in a state where no call with a state refinement is allowed */ FINAL_STATE, - /** The object's state is unknown, so these are the calls that lead to a state that allows the failing call */ - REACHING_CALLS + /** The object can be in any state: the state the failing call needs, and the constructors that create it */ + NEEDED_STATE } public static Hint general(String message) { diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/hints/StateHints.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/hints/StateHints.java index 72e9723b..f173b383 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/hints/StateHints.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/hints/StateHints.java @@ -2,11 +2,11 @@ import java.util.ArrayList; import java.util.Collection; -import java.util.LinkedHashMap; import java.util.List; -import java.util.Map; import java.util.Optional; import java.util.Set; +import java.util.TreeSet; +import java.util.function.Supplier; import java.util.stream.Collectors; import java.util.stream.Stream; @@ -17,8 +17,8 @@ import liquidjava.processor.state_machine.DecidingArgument; import liquidjava.processor.state_machine.State; import liquidjava.processor.state_machine.StateMachine; -import liquidjava.processor.state_machine.Transition; import liquidjava.utils.Utils; +import liquidjava.utils.constants.Keys; import spoon.reflect.reference.CtExecutableReference; import spoon.reflect.reference.CtTypeReference; @@ -35,10 +35,17 @@ public final class StateHints { private final StateMachine machine; private final String receiver; + /** The states that allow the failing call, grouped by the state refinement that allows it */ + private final List> goals; + /** The state sets the failing call checks, as indexes into {@link State#names()} */ + private final Set checkedSets; - private StateHints(StateMachine machine, String receiver) { + private StateHints(StateMachine machine, String receiver, RefinedFunction call) { this.machine = machine; this.receiver = receiver; + this.goals = machine.statesAllowingByRefinement(call); + this.checkedSets = goals.stream().flatMap(g -> machine.stateSetsNamed(g).stream()) + .collect(Collectors.toCollection(TreeSet::new)); } /** @@ -50,21 +57,24 @@ private StateHints(StateMachine machine, String receiver) { * the receiver as written in the code * @param category * the error's category, or {@code null} if it has none + * @param checkedElsewhere + * whether the receiver's state was checked elsewhere, though not decided, e.g. by an earlier call whose + * result says which state it is in */ public static List forCall(StateMachine machine, RefinedFunction call, Set current, String receiver, - ErrorCategory category) { + ErrorCategory category, boolean checkedElsewhere) { if (!machine.models(call) || current.isEmpty() || machine.allows(current, call)) return List.of(); // the machine cannot explain why the call failed - Set goal = machine.statesAllowing(call); - if (goal.isEmpty()) + StateHints hints = new StateHints(machine, receiver, call); + if (hints.goals.isEmpty()) return List.of(); - StateHints hints = new StateHints(machine, receiver); - if (category == ErrorCategory.UNKNOWN) - return hints.reachingCalls(call, goal); + if (category == ErrorCategory.UNKNOWN || checkedElsewhere) + return hints.anyState(current, call, checkedElsewhere); boolean pathDependent = category == ErrorCategory.PATH_DEPENDENT_STATE; - return Stream.concat(hints.howToReach(current, call, goal, pathDependent).stream(), - hints.allowedCalls(current).stream()).toList(); + List sequences = hints.howToReach(current, call, hints.namesHere(current), + () -> machine.complete() ? List.of(hints.unreachable(current, call, pathDependent)) : List.of()); + return Stream.concat(sequences.stream(), hints.allowedCalls(current).stream()).toList(); } /** The earlier call whose arguments decided the receiver's state, and values that would allow the call */ @@ -79,53 +89,64 @@ public static Hint decidingArgument(DecidingArgument deciding, String receiver) deciding.call().position().getLine(), receiver, values)); } - /** Nothing is known about the receiver's state: list what leads to a state where {@code call} is allowed */ - private List reachingCalls(RefinedFunction call, Set goal) { - Map> sources = new LinkedHashMap<>(); - for (Transition t : machine.transitionsEnabling(call)) - sources.computeIfAbsent(t.method(), m -> new ArrayList<>()).add(t.from()); - Stream constructors = machine.constructorsEnabling(call).stream().map(StateHints::constructor); - Stream calls = sources.entrySet().stream() - .map(e -> call(e.getKey()) + " (from " + names(e.getValue()) + ")"); - List ways = Stream.concat(constructors, calls).toList(); - if (ways.isEmpty()) - return List.of(); - return List.of(new Hint(Kind.REACHING_CALLS, String.format( - "The state of %s is unknown here. To get it to %s, use: %s", receiver, names(goal), list(ways)))); + /** + * The receiver can be in any state: name the state {@code call} needs and the calls that get there from any state. + * A call allowed in only some states is never suggested, since whether it is allowed is just as unknown. Calls that + * only tell which state the object is in are not in the machine, so no hint suggests checking one first. + * + * @param checkedElsewhere + * whether the state was checked, though the check did not decide it + */ + private List anyState(Set current, RefinedFunction call, boolean checkedElsewhere) { + String known = checkedElsewhere ? "What is known here does not decide the state of " + receiver + : "The state of " + receiver + " is unknown here"; + String message = known + ", and this call needs it to be " + needed(); + message += newObjects(call).map(c -> ". Objects created with " + c + " start in such a state").orElse(""); + List hints = new ArrayList<>(); + hints.add(new Hint(Kind.NEEDED_STATE, message)); + hints.addAll(howToReach(current, call, "any state", List::of)); + return hints; } - private List howToReach(Set current, RefinedFunction call, Set goal, boolean pathDependent) { + /** + * The shortest sequences of calls that are allowed in every state of {@code current} and lead to {@code call} + * + * @param from + * how to name {@code current} + * @param unreachable + * the hints to give if no sequence exists + */ + private List howToReach(Set current, RefinedFunction call, String from, + Supplier> unreachable) { Optional>> search = machine.shortestPaths(current, call, MAX_SEQUENCES); if (search.isEmpty()) return List.of(); List> sequences = search.get(); if (sequences.isEmpty()) - return machine.complete() ? List.of(unreachable(current, call, goal, pathDependent)) : List.of(); + return unreachable.get(); if (sequences.get(0).size() > MAX_SEQUENCE_LENGTH) return List.of(); - return sequences.stream().map(sequence -> callSequence(current, sequence)).toList(); + return sequences.stream().map(sequence -> callSequence(current, sequence, from)).toList(); } - private Hint callSequence(Set current, List sequence) { + private Hint callSequence(Set current, List sequence, String from) { Set reached = current; for (RefinedFunction method : sequence) reached = machine.after(reached, method); String calls = sequence.stream().map(this::call).collect(Collectors.joining(", then ")); return new Hint(Kind.CALL_SEQUENCE, String.format("Call %s before this call to move %s from %s to %s", calls, - receiver, names(current), names(reached))); + receiver, from, names(reached))); } - private Hint unreachable(Set current, RefinedFunction call, Set goal, boolean pathDependent) { + private Hint unreachable(Set current, RefinedFunction call, boolean pathDependent) { if (pathDependent) return new Hint(Kind.PATH_DEPENDENT_STATE, String.format( "%s can be in %s here, depending on the path taken, and no sequence of calls moves all of them to %s. " + "Make %s reach this line in the same state on every path", - receiver, names(current), names(goal), receiver)); - String message = String.format("No sequence of calls moves %s from %s to %s", receiver, names(current), - names(goal)); - List constructors = machine.constructorsEnabling(call).stream().map(StateHints::constructor).toList(); - if (!constructors.isEmpty()) - message += ". Create a new object instead with " + String.join(" or ", constructors); + receiver, namesHere(current), needed(), receiver)); + String message = String.format("No sequence of calls moves %s from %s to %s", receiver, namesHere(current), + needed()); + message += newObjects(call).map(c -> ". Create a new object instead with " + c).orElse(""); return new Hint(Kind.UNREACHABLE_STATE, message); } @@ -135,16 +156,24 @@ private List allowedCalls(Set current) { List signatures = allowed.stream().map(StateHints::signature).toList(); String others = machine.complete() ? "" : " (and possibly others)"; return List.of(new Hint(Kind.AVAILABLE_CALLS, String.format("In state %s, %s can call: %s%s", - names(current), receiver, list(signatures), others))); + namesHere(current), receiver, list(signatures), others))); } boolean noCallsInAnyState = current.stream().allMatch(s -> machine.allowedIn(Set.of(s)).isEmpty()); if (machine.complete() && noCallsInAnyState) return List.of(new Hint(Kind.FINAL_STATE, String.format("%s is in state %s, where none of its methods with state refinements can be called", - receiver, names(current)))); + receiver, namesHere(current)))); return List.of(); } + /** The constructors that create an object where {@code call} is allowed, unless the receiver is this object */ + private Optional newObjects(RefinedFunction call) { + if (receiver.equals(Keys.THIS)) + return Optional.empty(); + List constructors = machine.constructorsEnabling(call).stream().map(StateHints::constructor).toList(); + return constructors.isEmpty() ? Optional.empty() : Optional.of(String.join(" or ", constructors)); + } + private String call(RefinedFunction method) { return receiver + "." + signature(method); } @@ -163,8 +192,29 @@ private static String parameters(RefinedFunction function) { .collect(Collectors.joining(", ", "(", ")")); } - private static String names(Collection states) { - return states.stream().map(State::name).collect(Collectors.joining(" or ")); + /** {@code states} named as briefly as possible, e.g. {@code open or loud} */ + private String names(Collection states) { + return join(machine.describe(states)); + } + + /** The states the receiver can be in, named in the state sets the call checks and any set they all agree on */ + private String namesHere(Collection current) { + return join(machine.describe(current, checkedSets)); + } + + /** + * The states that allow the call. If every state does, each by a different state refinement, the states each + * refinement allows are named on their own: {@code a or b}, not every state. + */ + private String needed() { + Set goal = machine.ordered(goals.stream().flatMap(Set::stream).toList()); + if (goal.size() < machine.states().size()) + return names(goal); + return goals.stream().map(this::names).distinct().collect(Collectors.joining(" or ")); + } + + private static String join(List> groups) { + return groups.stream().map(group -> String.join(" and ", group)).collect(Collectors.joining(" or ")); } private static String list(List items) { diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/TypeChecker.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/TypeChecker.java index fb9efd2e..66a443dd 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/TypeChecker.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/TypeChecker.java @@ -430,6 +430,11 @@ private SMTResult verifyStateSMT(Predicate prevState, Predicate expectedState, S needsCounterexample); } + /** What a state refinement error from {@code found} to {@code expected} shows as found */ + public Predicate shownFound(Predicate found, Predicate expected) { + return vcChecker.shownFound(found, expected); + } + public void throwRefinementError(SourcePosition position, SourcePosition declarationPosition, Predicate expectedType, Predicate foundType, String customMessage) throws LJError { vcChecker.throwRefinementError(position, declarationPosition, expectedType, foundType, null, customMessage); diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/VCChecker.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/VCChecker.java index 819e4b6a..97289505 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/VCChecker.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/VCChecker.java @@ -446,6 +446,11 @@ protected void throwRefinementError(SourcePosition position, SourcePosition decl customMessage); } + /** What a state refinement error shows as found: what is known about the variables of both predicates */ + protected Predicate shownFound(Predicate found, Predicate expected) { + return buildPremiseChain(new TranslationTable(), expected, found).simplify().getImplication().toPredicate(); + } + protected void throwStateRefinementError(SourcePosition position, SourcePosition declarationPosition, Predicate found, Predicate expected, String customMessage, List hints, ErrorCategory category, StateErrorContext context) throws StateRefinementError { diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxStateHandler.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxStateHandler.java index 38fe52cd..6d17712b 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxStateHandler.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxStateHandler.java @@ -794,13 +794,16 @@ private static void changeState(TypeChecker tc, VariableInstance vi, RefinedFunc List ghostStates = getGhostStatesFor(function.getTargetClass(), tc); Optional deciding = decidingArgument(tc, vi, function, ghostStates, invocation); Optional states = receiverStates(tc, function, instanceName, prevState, invocation); - ErrorCategory category = deciding.isPresent() ? ErrorCategory.ARGUMENT_PICKS_THE_STATE - : states.flatMap( - r -> StateErrorCategories.categorize(r.machine(), r.current(), prevState, ghostStates)) - .orElse(null); + Predicate expected = expectedStatesDisjunction; + boolean checked = deciding.isEmpty() && states + .map(r -> checkedElsewhere(tc, r, prevState, expected, instanceName, ghostStates, invocation)) + .orElse(false); + ErrorCategory category = deciding.isPresent() ? ErrorCategory.ARGUMENT_PICKS_THE_STATE : states.flatMap( + r -> StateErrorCategories.categorize(r.machine(), r.current(), prevState, checked, ghostStates)) + .orElse(null); List hints = deciding.isPresent() ? receiverOf(invocation).map(r -> StateHints.decidingArgument(deciding.get(), r)).stream().toList() - : states.map(r -> stateHints(r, function, category, invocation)).orElse(List.of()); + : states.map(r -> stateHints(r, function, category, checked, invocation)).orElse(List.of()); StateErrorContext context = states .map(r -> StateErrorContext.of(r.machine(), function, r.current(), writtenReceiver(invocation))) .orElse(null); @@ -833,6 +836,19 @@ private static Optional receiverStates(TypeChecker tc, RefinedFu } } + /** Best effort, like {@link #receiverStates}: see {@link StateErrorCategories#checkedElsewhere} */ + private static boolean checkedElsewhere(TypeChecker tc, ReceiverStates states, Predicate found, Predicate expected, + String instanceName, List ghostStates, CtElement invocation) { + try { + return StateErrorCategories.checkedElsewhere(states.machine(), states.current(), found, + () -> tc.shownFound(found, expected), instanceName, ghostStates, + new StateSolver(tc, invocation.getPosition())); + } catch (RuntimeException e) { + DebugLog.warn("Could not tell whether the receiver's state was checked: " + e.getMessage()); + return false; + } + } + /** Best effort, like {@link #receiverStates} */ private static Optional decidingArgument(TypeChecker tc, VariableInstance receiver, RefinedFunction function, List ghostStates, CtElement invocation) { @@ -846,11 +862,11 @@ private static Optional decidingArgument(TypeChecker tc, Varia /** Hints on how to fix a call to {@code function} made in a state that does not allow it */ private static List stateHints(ReceiverStates states, RefinedFunction function, ErrorCategory category, - CtElement invocation) { + boolean checked, CtElement invocation) { Optional receiver = receiverOf(invocation); if (receiver.isEmpty() || !StateMachineBuilder.canModel(function)) return List.of(); - return StateHints.forCall(states.machine(), function, states.current(), receiver.get(), category); + return StateHints.forCall(states.machine(), function, states.current(), receiver.get(), category, checked); } /** diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/state_machine/StateCover.java b/liquidjava-verifier/src/main/java/liquidjava/processor/state_machine/StateCover.java new file mode 100644 index 00000000..4909824a --- /dev/null +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/state_machine/StateCover.java @@ -0,0 +1,152 @@ +package liquidjava.processor.state_machine; + +import java.util.ArrayList; +import java.util.Arrays; +import java.util.Comparator; +import java.util.HashSet; +import java.util.List; +import java.util.Set; +import java.util.TreeSet; +import java.util.stream.Collectors; +import java.util.stream.IntStream; + +/** + * Names a set of states as briefly as possible: as the fewest groups that each fix the state in some state sets and + * allow any state in the others. For example, the states where {@code open(this) || loud(this)} holds are named + * {@code open} or {@code loud}, not as every combination with the other state sets. + */ +final class StateCover { + + private static final int ANY = -1; + + /** + * States that fix the state of some state sets and allow any state in the others + * + * @param values + * the index of the fixed state in each state set, or {@link #ANY} + * @param members + * the states in the group + */ + private record Group(int[] values, Set members) { + } + + private final List states; + private final List> values; + + private StateCover(List states) { + this.states = states; + int stateSets = states.get(0).names().size(); + this.values = IntStream.range(0, stateSets) + .mapToObj(set -> states.stream().map(s -> s.names().get(set)).distinct().toList()).toList(); + } + + /** + * @param states + * every state of the class, one for each combination of the states of its state sets + * @param named + * the state sets every group must fix, as indexes into {@link State#names()} + * + * @return the groups, each given by the states it fixes, in the order the state sets are declared; if + * {@code subset} has every state and no set must be named, each state on its own + */ + static List> of(List states, Set subset, Set named) { + if (subset.isEmpty()) + return List.of(); + if (subset.size() == states.size() && named.isEmpty()) + return states.stream().map(State::names).toList(); + StateCover cover = new StateCover(states); + return cover.cover(subset, named).stream().map(cover::names).toList(); + } + + /** The state sets that the groups naming {@code subset} fix, as indexes into {@link State#names()} */ + static Set namedSets(List states, Set subset) { + if (subset.isEmpty()) + return Set.of(); + return new StateCover(states).cover(subset, Set.of()).stream().flatMap( + group -> IntStream.range(0, group.values().length).filter(set -> group.values()[set] != ANY).boxed()) + .collect(Collectors.toCollection(TreeSet::new)); + } + + /** The fewest of the largest groups inside {@code subset} that fix the sets {@code named} and hold all of it */ + private List cover(Set subset, Set named) { + List candidates = largestGroupsWithin(subset, named); + for (int size = 1;; size++) { + List chosen = firstCover(candidates, subset, size, 0, new ArrayList<>()); + if (chosen != null) + return chosen; + } + } + + /** The groups inside {@code subset} that fix the sets {@code named} and no larger such group holds */ + private List largestGroupsWithin(Set subset, Set named) { + List within = new ArrayList<>(); + groups(new int[values.size()], 0, within, subset, named); + return within.stream().filter(g -> within.stream().noneMatch(other -> other != g && contains(other, g))) + .sorted(declarationOrder()).toList(); + } + + /** Whether {@code larger} fixes fewer state sets than {@code smaller}, to the same states */ + private static boolean contains(Group larger, Group smaller) { + return !Arrays.equals(larger.values(), smaller.values()) && IntStream.range(0, larger.values().length) + .allMatch(set -> larger.values()[set] == ANY || larger.values()[set] == smaller.values()[set]); + } + + private void groups(int[] group, int set, List within, Set subset, Set named) { + if (set == values.size()) { + Set members = members(group); + if (subset.containsAll(members)) + within.add(new Group(group.clone(), members)); + return; + } + for (int value = named.contains(set) ? 0 : ANY; value < values.get(set).size(); value++) { + group[set] = value; + groups(group, set + 1, within, subset, named); + } + } + + /** The first {@code size} candidates from {@code next} on, in order, that hold all of {@code subset}, or null */ + private static List firstCover(List candidates, Set subset, int size, int next, + List chosen) { + if (chosen.size() == size) + return covers(chosen, subset) ? List.copyOf(chosen) : null; + for (int i = next; i < candidates.size(); i++) { + chosen.add(candidates.get(i)); + List found = firstCover(candidates, subset, size, i + 1, chosen); + chosen.remove(chosen.size() - 1); + if (found != null) + return found; + } + return null; + } + + private static boolean covers(List groups, Set subset) { + Set covered = new HashSet<>(); + groups.forEach(g -> covered.addAll(g.members())); + return covered.containsAll(subset); + } + + private Set members(int[] group) { + return states.stream() + .filter(s -> IntStream.range(0, group.length).allMatch( + set -> group[set] == ANY || values.get(set).get(group[set]).equals(s.names().get(set)))) + .collect(Collectors.toSet()); + } + + /** Groups fixing earlier state sets first, then by the order of the states within a set */ + private static Comparator declarationOrder() { + return (a, b) -> { + for (int set = 0; set < a.values().length; set++) { + int x = a.values()[set] == ANY ? Integer.MAX_VALUE : a.values()[set]; + int y = b.values()[set] == ANY ? Integer.MAX_VALUE : b.values()[set]; + if (x != y) + return Integer.compare(x, y); + } + return 0; + }; + } + + private List names(Group group) { + return IntStream.range(0, group.values().length).filter(set -> group.values()[set] != ANY) + .mapToObj(set -> values.get(set).get(group.values()[set])).toList(); + } +} diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/state_machine/StateErrorCategories.java b/liquidjava-verifier/src/main/java/liquidjava/processor/state_machine/StateErrorCategories.java index e0e1fbb8..03ff1d0a 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/state_machine/StateErrorCategories.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/state_machine/StateErrorCategories.java @@ -1,12 +1,18 @@ package liquidjava.processor.state_machine; +import java.util.LinkedHashSet; import java.util.List; import java.util.Optional; import java.util.Set; +import java.util.function.Supplier; import liquidjava.diagnostics.categories.ErrorCategory; +import liquidjava.diagnostics.errors.LJError; import liquidjava.processor.context.GhostState; import liquidjava.rj_language.Predicate; +import liquidjava.rj_language.ast.Expression; +import liquidjava.rj_language.ast.FunctionInvocation; +import liquidjava.rj_language.ast.Var; /** * The {@link ErrorCategory} of a call made in a state that does not allow it @@ -21,17 +27,19 @@ private StateErrorCategories() { * the states the receiver can be in before the call * @param found * what is known about the receiver before the call + * @param checkedElsewhere + * whether its state was only checked elsewhere, as told by {@link #checkedElsewhere} * @param ghostStates * the ghost states of the receiver's class * * @return the category, or nothing if it cannot be decided */ public static Optional categorize(StateMachine machine, Set current, Predicate found, - List ghostStates) { - List states = ghostStates.stream().filter(g -> g.getParent() != null).toList(); - // all states are possible and none is mentioned: nothing is known, which differs from a join of every state - if (current.size() == machine.states().size() && found.getStateInvocations(states).isEmpty()) - return Optional.of(ErrorCategory.UNKNOWN); + boolean checkedElsewhere, List ghostStates) { + List states = stateGhosts(ghostStates); + // nothing is known, which differs from a join of every state and from a check that did not decide the state + if (nothingMentioned(machine, current, found, states)) + return checkedElsewhere ? Optional.empty() : Optional.of(ErrorCategory.UNKNOWN); if (current.size() == 1) return Optional.of(ErrorCategory.OUT_OF_ORDER); // with several state sets, the states may differ only in a set the call does not check @@ -40,4 +48,50 @@ public static Optional categorize(StateMachine machine, Set current, Predicate found, + Supplier shownFound, String instance, List ghostStates, StateSolver solver) + throws LJError { + List states = stateGhosts(ghostStates); + if (!nothingMentioned(machine, current, found, states)) + return false; + Predicate shown = shownFound.get(); + Predicate receiver = Predicate.createVar(instance); + for (String object : objectsWithState(shown.getExpression(), states, new LinkedHashSet<>())) + if (object.equals(instance) + || solver.implies(shown, Predicate.createEquals(Predicate.createVar(object), receiver))) + return true; + return false; + } + + /** The variables that {@code expression} applies one of {@code states} to */ + private static Set objectsWithState(Expression expression, List states, Set objects) { + if (expression instanceof FunctionInvocation invocation + && states.stream().anyMatch(g -> g.matches(invocation.getName()))) + invocation.getArgs().stream().filter(Var.class::isInstance).map(v -> ((Var) v).getName()) + .forEach(objects::add); + expression.getChildren().forEach(child -> objectsWithState(child, states, objects)); + return objects; + } + + /** Whether every state is possible and {@code found} mentions none of them */ + private static boolean nothingMentioned(StateMachine machine, Set current, Predicate found, + List states) { + return current.size() == machine.states().size() && found.getStateInvocations(states).isEmpty(); + } + + private static List stateGhosts(List ghostStates) { + return ghostStates.stream().filter(g -> g.getParent() != null).toList(); + } } diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/state_machine/StateMachine.java b/liquidjava-verifier/src/main/java/liquidjava/processor/state_machine/StateMachine.java index 1bfa1926..524b079a 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/state_machine/StateMachine.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/state_machine/StateMachine.java @@ -66,7 +66,7 @@ public List allowedIn(Set current) { /** The states where {@code method} can be called */ public Set statesAllowing(RefinedFunction method) { - return ordered(transitions.stream().filter(t -> t.method().equals(method)).map(Transition::from).toList()); + return ordered(statesAllowingByRefinement(method).stream().flatMap(Set::stream).toList()); } /** The states the object can be in after calling {@code method}, which must be allowed in all of {@code current} */ @@ -107,16 +107,41 @@ public Optional>> shortestPaths(Set current, R return Optional.of(List.of()); } - /** The transitions from a state where {@code call} is not allowed to states where it is */ - public List transitionsEnabling(RefinedFunction call) { - return transitions.stream().filter(t -> !allows(Set.of(t.from()), call) && allows(t.to(), call)).toList(); - } - /** The constructors that create the object in a state where {@code call} is allowed */ public List constructorsEnabling(RefinedFunction call) { return constructors.entrySet().stream().filter(e -> allows(e.getValue(), call)).map(Map.Entry::getKey).toList(); } + /** + * {@code subset} named as briefly as possible, as groups of states that each fix the state in some state sets and + * allow any state in the others, e.g. {@code [[open], [loud]]} for the states where {@code open(this) || + * loud(this)} holds + */ + public List> describe(Collection subset) { + return describe(subset, Set.of()); + } + + /** Like {@link #describe(Collection)}, but naming the state of every set in {@code named} */ + public List> describe(Collection subset, Set named) { + return StateCover.of(states, Set.copyOf(subset), named); + } + + /** + * The state sets that {@code subset} depends on, as indexes into {@link State#names()}: those its + * {@link #describe(Collection) description} names + */ + public Set stateSetsNamed(Collection subset) { + return StateCover.namedSets(states, Set.copyOf(subset)); + } + + /** The states where {@code method} can be called, for each of its state refinements that applies in some state */ + public List> statesAllowingByRefinement(RefinedFunction method) { + Map> byChange = new LinkedHashMap<>(); + transitions.stream().filter(t -> t.method().equals(method)) + .forEach(t -> byChange.computeIfAbsent(t.change(), c -> new ArrayList<>()).add(t.from())); + return byChange.values().stream().map(this::ordered).toList(); + } + /** {@code subset} in declaration order */ public Set ordered(Collection subset) { return states.stream().filter(subset::contains).collect(Collectors.toCollection(LinkedHashSet::new)); diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/state_machine/StateMachineBuilder.java b/liquidjava-verifier/src/main/java/liquidjava/processor/state_machine/StateMachineBuilder.java index 617c4c4a..05314849 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/state_machine/StateMachineBuilder.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/state_machine/StateMachineBuilder.java @@ -19,7 +19,10 @@ import liquidjava.rj_language.Predicate; import liquidjava.utils.Utils; import liquidjava.utils.constants.Keys; +import spoon.reflect.declaration.CtClass; import spoon.reflect.declaration.CtElement; +import spoon.reflect.declaration.CtModifiable; +import spoon.reflect.declaration.CtType; import spoon.reflect.reference.CtExecutableReference; import spoon.reflect.reference.CtTypeReference; @@ -131,6 +134,8 @@ private StateMachine build(String className, CtTypeReference type) throws LJE if (!className.equals(function.getTargetClass()) || !function.hasStateChange()) continue; if (CtExecutableReference.CONSTRUCTOR_NAME.equals(function.getName())) { + if (abstractType(type) || privateConstructor(function, type)) + continue; // cannot be suggested as a new object Optional> created = createdStates(function); created.ifPresent(s -> constructors.put(function, s)); continue; @@ -154,6 +159,36 @@ private boolean relatedClassChangesState(String className, CtTypeReference ty .anyMatch(other -> other.isSubtypeOf(type) || type.isSubtypeOf(other)); } + private static boolean abstractType(CtTypeReference type) { + CtType declaration = type.getTypeDeclaration(); + return declaration == null || declaration.isInterface() || declaration.isAbstract(); + } + + /** + * Whether {@code constructor} cannot be called from outside its class: it is private, or the class is an enum. A + * constructor that is not found in the class's declaration is assumed callable. The machine is shared by every + * caller, so a private constructor is left out even for calls inside its class. + */ + private static boolean privateConstructor(RefinedFunction constructor, CtTypeReference type) { + try { + CtType declaration = type.getTypeDeclaration(); + if (declaration.isEnum()) + return true; + if (!(declaration instanceof CtClass declared)) + return false; + List parameters = constructor.getArguments().stream().map(a -> typeName(a.getType())).toList(); + return declared.getConstructors().stream() + .filter(c -> c.getParameters().stream().map(p -> typeName(p.getType())).toList().equals(parameters)) + .anyMatch(CtModifiable::isPrivate); + } catch (RuntimeException e) { + return false; // a declaration that cannot be built is not evidence that the constructor is private + } + } + + private static String typeName(CtTypeReference type) { + return type == null ? "" : type.getQualifiedName(); + } + /** The transitions of {@code method}, or nothing if they depend on more than the state of {@code this} */ private Optional> transitionsOf(RefinedFunction method) throws LJError { if (!canModel(method)) diff --git a/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestStateHints.java b/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestStateHints.java index 8f5b4282..ce9eded2 100644 --- a/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestStateHints.java +++ b/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestStateHints.java @@ -3,11 +3,13 @@ import static org.junit.jupiter.api.Assertions.*; import java.util.List; +import java.util.Optional; import org.junit.jupiter.api.Test; import liquidjava.api.CommandLineLauncher; import liquidjava.diagnostics.Diagnostics; +import liquidjava.diagnostics.categories.ErrorCategory; import liquidjava.diagnostics.errors.LJError; import liquidjava.diagnostics.errors.StateRefinementError; import liquidjava.diagnostics.hints.Hint; @@ -85,9 +87,78 @@ void receiverThatIsNotAVariableGetsNoHints() { } @Test - void unknownStateListsTheCallsThatLeadToTheExpectedState() { - assertHints("ErrorStateHintUnknownState.java", new Hint(Kind.REACHING_CALLS, - "The state of f is unknown here. To get it to open, use: f.open() (from created)")); + void unknownStateDoesNotSuggestACallThatNeedsAnotherUnknownState() { + assertHints("ErrorStateHintUnknownState.java", + new Hint(Kind.NEEDED_STATE, "The state of f is unknown here, and this call needs it to be open")); + } + + @Test + void unknownStateOfAnExternalClassNamesOnlyTheCheckedStateSet() { + assertHints("classes/state_hint_undo_manager_error", new Hint(Kind.NEEDED_STATE, + "The state of undoManager is unknown here, and this call needs it to be redoable")); + } + + @Test + void unknownStateSuggestsCallsAllowedInAnyState() { + assertHints("ErrorStateHintUnknownAnyState.java", + new Hint(Kind.NEEDED_STATE, "The state of f is unknown here, and this call needs it to be open"), + new Hint(Kind.CALL_SEQUENCE, + "Call f.reset(), then f.open() before this call to move f from any state to open")); + } + + @Test + void statesAreNamedOnlyInTheStateSetsThatMatter() { + List errors = errors("ErrorStateHintNaming.java", 3); + assertHints(errors.get(0), new Hint(Kind.NEEDED_STATE, + "The state of s is unknown here, and this call needs it to be open or loud")); + assertHints(errors.get(1), + new Hint(Kind.NEEDED_STATE, "The state of t is unknown here, and this call needs it to be a or b. " + + "Objects created with new ErrorStateHintNamingToggle() start in such a state")); + assertHints(errors.get(2), + new Hint(Kind.UNREACHABLE_STATE, "No sequence of calls moves this from notRedoable to redoable"), + new Hint(Kind.AVAILABLE_CALLS, "In state notRedoable, this can call: check()")); + } + + @Test + void failedCheckOfTheReceiverIsNotAnUnknownState() { + List errors = errors("classes/state_hint_checked_error", 3); + assertHints(errors.get(0), new Hint(Kind.NEEDED_STATE, + "What is known here does not decide the state of it, and this call needs it to be hasMore")); + assertHints(errors.get(1), new Hint(Kind.NEEDED_STATE, + "What is known here does not decide the state of same, and this call needs it to be hasMore")); + assertHints(errors.get(2), new Hint(Kind.NEEDED_STATE, + "The state of input is unknown here, and this call needs it to be hasMore")); + assertEquals(List.of(Optional.empty(), Optional.empty(), Optional.of(ErrorCategory.UNKNOWN)), + errors.stream().map(LJError::getCategory).toList()); + } + + @Test + void joinsAreNotTakenForAnUnknownState() { + List errors = errors("ErrorStateHintJoins.java", 2); + assertHints(errors.get(0), new Hint(Kind.UNREACHABLE_STATE, + "No sequence of calls moves d from closed and unlocked or closed and locked or opened and unlocked " + + "or opened and locked to closed and unlocked. " + + "Create a new object instead with new ErrorStateHintJoins()")); + assertHints(errors.get(1), new Hint(Kind.UNREACHABLE_STATE, + "No sequence of calls moves d from closed and unlocked or opened and unlocked to closed and unlocked. " + + "Create a new object instead with new ErrorStateHintJoins()"), + new Hint(Kind.AVAILABLE_CALLS, + "In state closed and unlocked or opened and unlocked, d can call: lock()")); + assertEquals(Optional.empty(), errors.get(0).getCategory()); + } + + @Test + void onlyConstructorsThatCanBeCalledAreSuggested() { + List errors = errors("ErrorStateHintConstructors.java", 4); + assertHints(errors.get(0), + new Hint(Kind.NEEDED_STATE, "The state of value is unknown here, and this call needs it to be ready. " + + "Objects created with new ErrorStateHintConstructors() start in such a state")); + assertHints(errors.get(1), + new Hint(Kind.NEEDED_STATE, "The state of this is unknown here, and this call needs it to be ready")); + assertHints(errors.get(2), + new Hint(Kind.NEEDED_STATE, "The state of value is unknown here, and this call needs it to be ready")); + assertHints(errors.get(3), + new Hint(Kind.NEEDED_STATE, "The state of value is unknown here, and this call needs it to be ready")); } @Test @@ -109,10 +180,18 @@ void classWithoutStateSetKeepsTheGeneralHint() { } private static void assertHints(String test, Hint... expected) { + assertHints(errors(test, 1).get(0), expected); + } + + private static void assertHints(StateRefinementError error, Hint... expected) { + assertEquals(List.of(expected), error.getHints()); + } + + /** The {@code count} errors {@code test} reports, in the order they are reported */ + private static List errors(String test, int count) { CommandLineLauncher.launch(TEST_SUITE + test); List errors = Diagnostics.getInstance().getErrors().stream().toList(); - assertEquals(1, errors.size(), "Expected exactly one error from " + test); - StateRefinementError error = assertInstanceOf(StateRefinementError.class, errors.get(0)); - assertEquals(List.of(expected), error.getHints()); + assertEquals(count, errors.size(), "Unexpected number of errors from " + test); + return errors.stream().map(e -> assertInstanceOf(StateRefinementError.class, e)).toList(); } } diff --git a/liquidjava-verifier/src/test/java/liquidjava/processor/state_machine/StateMachineTest.java b/liquidjava-verifier/src/test/java/liquidjava/processor/state_machine/StateMachineTest.java new file mode 100644 index 00000000..24d4db72 --- /dev/null +++ b/liquidjava-verifier/src/test/java/liquidjava/processor/state_machine/StateMachineTest.java @@ -0,0 +1,102 @@ +package liquidjava.processor.state_machine; + +import static org.junit.jupiter.api.Assertions.assertEquals; + +import java.util.ArrayList; +import java.util.List; +import java.util.Map; +import java.util.Set; + +import org.junit.jupiter.api.Test; + +import liquidjava.rj_language.Predicate; + +class StateMachineTest { + + // two state sets, {open, closed} and {locked, unlocked}, combined in declaration order + private static final State OPEN_LOCKED = state("open", "locked"); + private static final State OPEN_UNLOCKED = state("open", "unlocked"); + private static final State CLOSED_LOCKED = state("closed", "locked"); + private static final State CLOSED_UNLOCKED = state("closed", "unlocked"); + private static final StateMachine MACHINE = machine( + List.of(OPEN_LOCKED, OPEN_UNLOCKED, CLOSED_LOCKED, CLOSED_UNLOCKED)); + + @Test + void statesDifferingOnlyInOneSetAreNamedByTheOther() { + assertEquals(List.of(List.of("open")), MACHINE.describe(Set.of(OPEN_LOCKED, OPEN_UNLOCKED))); + assertEquals(List.of(List.of("unlocked")), MACHINE.describe(Set.of(OPEN_UNLOCKED, CLOSED_UNLOCKED))); + } + + @Test + void singleStateIsNamedInEverySet() { + assertEquals(List.of(List.of("closed", "unlocked")), MACHINE.describe(Set.of(CLOSED_UNLOCKED))); + } + + @Test + void statesDifferingInBothSetsAreNamedInBoth() { + assertEquals(List.of(List.of("open", "locked"), List.of("closed", "unlocked")), + MACHINE.describe(Set.of(CLOSED_UNLOCKED, OPEN_LOCKED))); + } + + @Test + void disjunctionAcrossSetsNamesEachStateAlone() { + // open || locked + assertEquals(List.of(List.of("open"), List.of("locked")), + MACHINE.describe(Set.of(OPEN_LOCKED, OPEN_UNLOCKED, CLOSED_LOCKED))); + } + + @Test + void everyStateIsNamedStateByState() { + assertEquals(List.of(List.of("open", "locked"), List.of("open", "unlocked"), List.of("closed", "locked"), + List.of("closed", "unlocked")), MACHINE.describe(Set.copyOf(MACHINE.states()))); + } + + @Test + void statesAreNamedInEverySetAsked() { + // the states differ in the first set, which must still be named + assertEquals(List.of(List.of("open", "unlocked"), List.of("closed", "unlocked")), + MACHINE.describe(Set.of(OPEN_UNLOCKED, CLOSED_UNLOCKED), Set.of(0))); + assertEquals(List.of(List.of("open"), List.of("closed")), + MACHINE.describe(Set.copyOf(MACHINE.states()), Set.of(0))); + } + + @Test + void setsNamedAreThoseTheDescriptionFixes() { + assertEquals(Set.of(1), MACHINE.stateSetsNamed(Set.of(OPEN_UNLOCKED, CLOSED_UNLOCKED))); + assertEquals(Set.of(0, 1), MACHINE.stateSetsNamed(Set.of(OPEN_LOCKED, OPEN_UNLOCKED, CLOSED_LOCKED))); + assertEquals(Set.of(), MACHINE.stateSetsNamed(Set.of())); + } + + @Test + void noStatesAreNamedByNothing() { + assertEquals(List.of(), MACHINE.describe(Set.of())); + } + + @Test + void disjunctionOverThreeSetsNamesOnlyTheCheckedStates() { + // {start, canEdit, end} x {undoable, notUndoable} x {redoable, notRedoable}, and undoable || redoable + List states = new ArrayList<>(); + for (String edit : List.of("start", "canEdit", "end")) + for (String undo : List.of("undoable", "notUndoable")) + for (String redo : List.of("redoable", "notRedoable")) + states.add(state(edit, undo, redo)); + Set goal = Set.copyOf(states.stream() + .filter(s -> s.names().get(1).equals("undoable") || s.names().get(2).equals("redoable")).toList()); + assertEquals(List.of(List.of("undoable"), List.of("redoable")), machine(states).describe(goal)); + } + + @Test + void statesOfOneSetAreNamedInDeclarationOrder() { + List states = List.of(state("s0"), state("s1"), state("s2"), state("s3")); + assertEquals(List.of(List.of("s1"), List.of("s3")), + machine(states).describe(Set.of(states.get(3), states.get(1)))); + } + + private static StateMachine machine(List states) { + return new StateMachine(states, List.of(), List.of(), Map.of(), true); + } + + private static State state(String... names) { + return new State(List.of(names), new Predicate()); + } +}