diff --git a/liquidjava-example/src/main/java/testSuite/CorrectStateValues.java b/liquidjava-example/src/main/java/testSuite/CorrectStateValues.java new file mode 100644 index 00000000..42ce986e --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/CorrectStateValues.java @@ -0,0 +1,105 @@ +package testSuite; + +import liquidjava.specification.Refinement; +import liquidjava.specification.RefinementAlias; +import liquidjava.specification.StateRefinement; +import liquidjava.specification.StateSet; + +// an unrelated set with the same name and other states, in a class whose sets are listed before those of +// CorrectStateValues +@StateSet(name = "door", value = {"ajar", "shut"}) +class CorrectStateValueDoor {} + +@StateSet(name = "door", value = {"closed", "opened"}) +@StateSet(name = "lock", value = {"unlocked", "locked"}) +@RefinementAlias("Shut(CorrectStateValues d) { door(d) == closed }") +public class CorrectStateValues { + + @StateRefinement(to = "door(this) == closed && lock(this) == unlocked") + public CorrectStateValues() {} + + @StateRefinement(from = "door(this) == closed && lock(this) != locked", to = "door(this) == opened") + public void open() {} + + // the set can also be applied as a method of this, or with this left out + @StateRefinement(from = "this.door() == opened", to = "door() == closed") + public void close() {} + + // when it fails, the lock set keeps its value + @StateRefinement(from = "door(this) == closed", to = "return ? lock(this) == locked : lock(this) == lock(old(this))") + public boolean tryLock() { + return true; + } + + @StateRefinement(from = "locked == this.lock()", to = "lock() != locked") + public void unlock() {} + + // the parameter closed keeps its meaning: the door takes its value + @StateRefinement(to = "door(this) == closed") + public void choose(int closed) {} + + static void needsShut(@Refinement("Shut(_)") CorrectStateValues d) {} + + public static void main(String[] args) { + CorrectStateValues d = new CorrectStateValues(); + int closed = 1; // the alias body still means the state closed + needsShut(d); + d.open(); + d.close(); + if (d.tryLock()) + d.unlock(); + d.open(); + d.choose(1); + d.close(); + } +} + +// states named like the variables _ and return do not take their place +@StateSet(name = "mode", value = {"_", "return", "on"}) +class CorrectStateValueVariableNames { + + @StateRefinement(to = "mode(this) == on") + public CorrectStateValueVariableNames() {} + + public void check(@Refinement("mode(this) == _") int value) {} + + @Refinement("_ == 2") + @StateRefinement(to = "mode(this) == return") + public int pick() { + return 2; + } + + @StateRefinement(from = "mode(this) == on") + public void needsOn() {} + + static void test() { + CorrectStateValueVariableNames v = new CorrectStateValueVariableNames(); + v.check(2); + v.pick(); + v.needsOn(); + } +} + +// a subclass uses the set of its superclass, not the unrelated one with the same name +class CorrectStateValueSubclass extends CorrectStateValues { + + @StateRefinement(from = "door(this) == opened", to = "door(this) == closed") + public void shut() {} + + static void test() { + CorrectStateValueSubclass s = new CorrectStateValueSubclass(); + s.open(); + s.shut(); + } +} + +// a subclass that declares its own set named door uses its states, as the shorthand does +@StateSet(name = "door", value = {"open", "closed"}) +class CorrectStateValueBase {} + +@StateSet(name = "door", value = {"ajar", "shut"}) +class CorrectStateValueChild extends CorrectStateValueBase { + + @StateRefinement(from = "door(this) == shut", to = "door(this) == ajar") + public void push() {} +} diff --git a/liquidjava-example/src/main/java/testSuite/ErrorStateValueQuery.java b/liquidjava-example/src/main/java/testSuite/ErrorStateValueQuery.java new file mode 100644 index 00000000..a32f76c2 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/ErrorStateValueQuery.java @@ -0,0 +1,23 @@ +package testSuite; + +import liquidjava.specification.Refinement; +import liquidjava.specification.StateRefinement; +import liquidjava.specification.StateSet; + +// a query written with its state set is offered as a guard, like one written with the state +@StateSet(name = "lock", value = {"unlocked", "locked"}) +public abstract class ErrorStateValueQuery { + + @StateRefinement(to = "lock(this) == locked") + public ErrorStateValueQuery() {} + + @StateRefinement(from = "lock(this) == unlocked") + public void open() {} + + @Refinement("_ == true --> lock(this) == unlocked") + public abstract boolean isUnlocked(); + + static void use(ErrorStateValueQuery d) { + d.open(); // Expect: State Refinement Error + } +} diff --git a/liquidjava-example/src/main/java/testSuite/ErrorStateValues.java b/liquidjava-example/src/main/java/testSuite/ErrorStateValues.java new file mode 100644 index 00000000..a75242fd --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/ErrorStateValues.java @@ -0,0 +1,38 @@ +package testSuite; + +import liquidjava.specification.StateRefinement; +import liquidjava.specification.StateSet; + +@StateSet(name = "door", value = {"closed", "opened"}) +@StateSet(name = "lock", value = {"unlocked", "locked"}) +public class ErrorStateValues { + + @StateRefinement(from = "door(this) == locked") // Expect: Error + public void wrongSet() {} +} + +@StateSet({"closed", "open"}) +@StateSet({"open", "locked"}) // Expect: Error +class ErrorStateValuesSharedState {} + +@StateSet({"state1", "open"}) // Expect: Error +class ErrorStateValuesGeneratedSetName {} + +// an unrelated set named door that has a state locked does not make locked a state of the door above +@StateSet(name = "door", value = {"locked", "free"}) +class ErrorStateValuesOtherDoor {} + +// the set applied as a method of this, or with this left out, constrains the same state +@StateSet(name = "door", value = {"shut", "ajar"}) +class ErrorStateValueForms { + + @StateRefinement(to = "door() == shut") + public ErrorStateValueForms() {} + + @StateRefinement(from = "this.door() == ajar") + public void close() {} + + static void test() { + new ErrorStateValueForms().close(); // Expect: State Refinement Error + } +} diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/context/AliasWrapper.java b/liquidjava-verifier/src/main/java/liquidjava/processor/context/AliasWrapper.java index 0578e62b..120bc475 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/context/AliasWrapper.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/context/AliasWrapper.java @@ -29,10 +29,13 @@ public AliasWrapper(AliasDTO a, Factory factory, String klass, String path, Sour this.position = position; varTypes = new ArrayList<>(); varNames = a.getVarNames(); - for (String s : a.getVarTypes()) { - CtTypeReference r = Utils.getType(s.equals(klass) ? path : s, factory); - varTypes.add(r); - } + for (String s : a.getVarTypes()) + varTypes.add(parameterType(s, factory, klass, path)); + } + + /** The type of an alias parameter written {@code type}, in an alias declared on class {@code klass} at path */ + public static CtTypeReference parameterType(String type, Factory factory, String klass, String path) { + return Utils.getType(type.equals(klass) ? path : type, factory); } public String getName() { diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/facade/AliasDTO.java b/liquidjava-verifier/src/main/java/liquidjava/processor/facade/AliasDTO.java index 9089873a..71ebeeb2 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/facade/AliasDTO.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/facade/AliasDTO.java @@ -5,6 +5,7 @@ import liquidjava.diagnostics.errors.LJError; import liquidjava.rj_language.Predicate; +import liquidjava.rj_language.StateValues; import liquidjava.rj_language.ast.Expression; import liquidjava.rj_language.parsing.RefinementsParser; import spoon.reflect.cu.SourcePosition; @@ -50,6 +51,15 @@ public void resolveStaticFinalConstants(CtElement context, SourcePosition positi } } + // Read the states written as values of their sets, phase(x) == open, as the shorthand open(x), with only the + // alias's + // parameters as variables, so a variable where the alias is used cannot take the place of a state + public void readStateValues(StateValues values) throws LJError { + if (expression != null) { + this.expression = values.toShorthand(expression); + } + } + public String getName() { return name; } 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 243adf1e..85c0657c 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 @@ -24,6 +24,10 @@ import liquidjava.processor.state_machine.StateMachineBuilder; import liquidjava.processor.state_machine.StateSolver; import liquidjava.rj_language.Predicate; +import liquidjava.rj_language.StateValues; +import liquidjava.rj_language.ast.Expression; +import liquidjava.rj_language.ast.FunctionInvocation; +import liquidjava.rj_language.ast.Var; import liquidjava.rj_language.ast.formatter.FieldDisplayNames; import liquidjava.rj_language.parsing.RefinementsParser; import liquidjava.smt.SMTEvaluator; @@ -39,8 +43,10 @@ import spoon.reflect.declaration.CtAnnotation; import spoon.reflect.declaration.CtClass; import spoon.reflect.declaration.CtElement; +import spoon.reflect.declaration.CtExecutable; import spoon.reflect.declaration.CtInterface; import spoon.reflect.declaration.CtMethod; +import spoon.reflect.declaration.CtParameter; import spoon.reflect.declaration.CtTypedElement; import spoon.reflect.declaration.CtVariable; import spoon.reflect.declaration.CtType; @@ -126,6 +132,7 @@ public Optional getRefinementFromAnnotation(CtElement element) throws String prefix = getQualifiedClassName(element); Predicate p = prefix == null ? new Predicate(ref.get(), element) : new Predicate(ref.get(), element, prefix); + p = readStateValues(p, element, Utils.getLJAnnotationPosition(element, ref.get())); if (!p.getExpression().isBooleanExpression()) { SourcePosition position = Utils.getLJAnnotationPosition(element, ref.get()); throw new InvalidRefinementError(position, "Refinement predicate must be a boolean expression", @@ -196,7 +203,8 @@ public Optional getMessageFromAnnotation(CtElement element) { @SuppressWarnings("unchecked") public void registerGhostsAndStateSets(CtElement element) throws LJError { int set = 0; - Map namedSets = new LinkedHashMap<>(); + Map stateSets = new LinkedHashMap<>(); + Map setOfState = new HashMap<>(); for (CtAnnotation ann : element.getAnnotations()) { String an = ann.getAnnotationType().getQualifiedName(); if (an.contentEquals("liquidjava.specification.StateSet")) { @@ -204,10 +212,10 @@ public void registerGhostsAndStateSets(CtElement element) throws LJError { CtExpression nameValue = ann.getValues().get("name"); SourcePosition namePosition = nameValue == null ? null : Utils.getAnnotationValuePosition(nameValue); String name = stateSetName(nameValue, namePosition); - GhostFunction g = createStateSet((CtNewArray) ann.getAllValues().get("value"), - name != null ? name : String.format("state%d", set), element); - if (name != null) - namedSets.put(g, namePosition); + CtNewArray states = (CtNewArray) ann.getAllValues().get("value"); + GhostFunction g = createStateSet(states, name != null ? name : String.format("state%d", set), element); + stateSets.put(g, name != null ? namePosition : Utils.getAnnotationValuePosition(states)); + checkStatesAreNotInAnotherSet(g, states, setOfState); } if (an.contentEquals("liquidjava.specification.Ghost")) { CtLiteral s = (CtLiteral) ann.getAllValues().get("value"); @@ -219,9 +227,28 @@ public void registerGhostsAndStateSets(CtElement element) throws LJError { Utils.getAnnotationValuePosition(rawValue)); } } - // checked once every set and ghost of the class exists, so the order of the annotations does not matter - for (Map.Entry named : namedSets.entrySet()) - checkStateSetNameIsFree(named.getKey(), named.getValue()); + // checked once every set and ghost of the class exists, so the order of the annotations does not matter; a + // generated name such as state1 can clash too + for (Map.Entry stateSet : stateSets.entrySet()) + checkStateSetNameIsFree(stateSet.getKey(), stateSet.getValue()); + } + + /** + * Reports a state of {@code set} that another set of its class also has: {@code open(this)} could not tell which of + * the two sets it is about + */ + private static void checkStatesAreNotInAnotherSet(GhostFunction set, CtNewArray states, + Map setOfState) throws LJError { + for (CtExpression state : states.getElements()) { + if (!(state instanceof CtLiteral literal && literal.getValue()instanceof String name)) + continue; + GhostFunction other = setOfState.putIfAbsent(name, set); + if (other != null) + throw new CustomError( + String.format("State '%s' is in two state sets of %s: %s and %s", name, + set.getParentClassName(), other.getName(), set.getName()), + Utils.getAnnotationValuePosition(literal)); + } } /** The name given to a state set, or null when it has none */ @@ -361,6 +388,72 @@ protected void getGhostFunction(String value, CtElement element, SourcePosition context.addGhostFunction(new GhostFunction(f, factory, type.getQualifiedName())); } + /** + * {@code p} with each state written as a value of its set, {@code phase(x) == open}, read as the shorthand + * {@code open(x)}, in the scope of {@code element}, whose variables keep their meaning + */ + public Predicate readStateValues(Predicate p, CtElement element, SourcePosition position) throws LJError { + StateValues values = new StateValues(context.getGhostStates(), name -> isVariableIn(element, name), + argument -> typeIn(element, argument).map(type -> set -> isOfType(type, set.getPrefix()))); + try { + return new Predicate(values.toShorthand(p.getExpression())); + } catch (LJError e) { + if (e.getPosition() == null) + e.setPosition(position); + throw e; + } + } + + /** + * Whether {@code name} is a variable where {@code element} is: a parameter, _, this, return, or one in the context + */ + private boolean isVariableIn(CtElement element, String name) { + if (name.equals(Keys.WILDCARD) || name.equals(Keys.THIS) || name.equals("return") || context.hasVariable(name)) + return true; + CtExecutable executable = element instanceof CtExecutable e ? e : element.getParent(CtExecutable.class); + return executable != null && executable.getParameters().stream().anyMatch(p -> p.getSimpleName().equals(name)); + } + + /** The type of a state's argument where {@code element} is: this, _, a parameter, a variable, or old of one */ + private Optional> typeIn(CtElement element, Expression argument) { + if (argument instanceof FunctionInvocation old && old.getName().equals(Keys.OLD) && old.getArgs().size() == 1) + return typeIn(element, old.getArgs().get(0)); + if (!(argument instanceof Var var)) + return Optional.empty(); + String name = var.getName(); + if (name.equals(Keys.THIS)) + return Optional.ofNullable(getQualifiedClassName(element)).map(c -> factory.Type().createReference(c)); + if (name.equals(Keys.WILDCARD)) + return element instanceof CtTypedElement typed ? Optional.ofNullable(typed.getType()) : Optional.empty(); + CtExecutable executable = element instanceof CtExecutable e ? e : element.getParent(CtExecutable.class); + if (executable != null) + for (CtParameter parameter : executable.getParameters()) + if (parameter.getSimpleName().equals(name)) + return Optional.ofNullable(parameter.getType()); + return context.hasVariable(name) ? Optional.ofNullable(context.getVariableByName(name).getType()) + : Optional.empty(); + } + + /** + * Reads the states written as values of their sets in the body of {@code alias}, declared on class {@code klass} at + * {@code path}: only its parameters are variables, typed as they are declared + */ + private StateValues aliasStateValues(AliasDTO alias, String klass, String path) { + return new StateValues(context.getGhostStates(), alias.getVarNames()::contains, argument -> { + int parameter = argument instanceof Var var ? alias.getVarNames().indexOf(var.getName()) : -1; + if (parameter < 0) + return Optional.empty(); + CtTypeReference type = AliasWrapper.parameterType(alias.getVarTypes().get(parameter), factory, klass, + path); + return Optional.of(set -> isOfType(type, set.getPrefix())); + }); + } + + /** Whether {@code type} is the class {@code className} or one of its subtypes */ + private boolean isOfType(CtTypeReference type, String className) { + return type.getQualifiedName().equals(className) || type.isSubtypeOf(factory.Type().createReference(className)); + } + protected void handleAlias(String ref, CtElement element, SourcePosition position) throws LJError { try { AliasDTO a = RefinementsParser.parseAliasDefinition(ref); @@ -376,6 +469,7 @@ protected void handleAlias(String ref, CtElement element, SourcePosition positio if (klass != null && path != null) { a.parse(path); a.resolveStaticFinalConstants(element, position); + a.readStateValues(aliasStateValues(a, klass, path)); if (a.getExpression() != null && !a.getExpression().isBooleanExpression()) { throw new InvalidRefinementError(position, "Refinement alias must return a boolean expression", ref); 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 f1ce3d1c..c2d00a08 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 @@ -56,7 +56,7 @@ public static void handleConstructorState(CtConstructor c, RefinedFunction f, throw new IllegalConstructorTransitionError(Utils.getAnnotationValuePosition(from)); } } - setConstructorStates(f, an, c); + setConstructorStates(f, an, c, tc); } else if (!inheritSuperConstructorState(c, f, tc)) { setDefaultState(f, tc); } @@ -283,7 +283,7 @@ private static List> typeReferences(TypeChecker tc, List> anns, - CtElement element) throws LJError { + CtElement element, TypeChecker tc) throws LJError { List l = new ArrayList<>(); for (CtAnnotation an : anns) { Map m = an.getAllValues(); @@ -294,7 +294,8 @@ private static void setConstructorStates(RefinedFunction f, List ctAnnota private static Predicate createStatePredicate(Predicate p, String value, String targetClass, TypeChecker tc, CtElement e, boolean isTo) throws LJError { SourcePosition position = Utils.getLJAnnotationPosition(e, value); + p = tc.readStateValues(p, e, position); if (!p.getExpression().isBooleanExpression()) { throw new InvalidRefinementError(position, "State refinement transition must be a boolean expression", value); diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/StateValues.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/StateValues.java new file mode 100644 index 00000000..abcc8236 --- /dev/null +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/StateValues.java @@ -0,0 +1,109 @@ +package liquidjava.rj_language; + +import java.util.List; +import java.util.Objects; +import java.util.Optional; +import java.util.function.Function; +import java.util.function.Predicate; +import java.util.stream.Collectors; + +import liquidjava.diagnostics.errors.CustomError; +import liquidjava.diagnostics.errors.LJError; +import liquidjava.processor.context.GhostFunction; +import liquidjava.processor.context.GhostState; +import liquidjava.rj_language.ast.BinaryExpression; +import liquidjava.rj_language.ast.Expression; +import liquidjava.rj_language.ast.FunctionInvocation; +import liquidjava.rj_language.ast.UnaryExpression; +import liquidjava.rj_language.ast.Var; + +/** + * Reads a state written as a value of its state set, {@code phase(e) == open}, as the state shorthand {@code open(e)}, + * so that everything that reads states sees one form + */ +public final class StateValues { + + private final List states; + private final Predicate isVariable; + private final Function>> setsFor; + + /** + * @param isVariable + * whether a name is a variable where the spec is written; a variable keeps its meaning + * @param setsFor + * the state sets that can be applied to an argument, by its type, or empty when its type is not known + */ + public StateValues(List states, Predicate isVariable, + Function>> setsFor) { + this.states = states; + this.isVariable = isVariable; + this.setsFor = setsFor; + } + + /** + * {@code expression} with each {@code set(e) == state} read as {@code state(e)} and each {@code set(e) != state} as + * {@code !state(e)} + * + * @throws CustomError + * when the name is not a variable and is a state of another set of the same class + */ + public Expression toShorthand(Expression expression) throws LJError { + return rewrite(expression.clone()); + } + + private Expression rewrite(Expression e) throws LJError { + if (e instanceof BinaryExpression b && (b.getOperator().equals("==") || b.getOperator().equals("!="))) { + Optional state = stateOf(b.getFirstOperand(), b.getSecondOperand()); + if (state.isEmpty()) + state = stateOf(b.getSecondOperand(), b.getFirstOperand()); + if (state.isPresent()) + return b.getOperator().equals("==") ? state.get() : new UnaryExpression("!", state.get()); + } + for (int i = 0; i < e.getChildren().size(); i++) + e.setChild(i, rewrite(e.getChildren().get(i))); + return e; + } + + /** + * {@code state(e)} when {@code set} is a state set applied to {@code e} and {@code name} a state of a set of that + * name that applies to the type of {@code e}, or, when that type is not known, of every set of that name. It is + * named as the shorthand written in the same place, so that it is resolved the same way, in a subclass too. + * Otherwise nothing is read, and the name stays an unknown variable + */ + private Optional stateOf(Expression set, Expression name) throws LJError { + if (!(set instanceof FunctionInvocation invocation && invocation.getArgs().size() == 1 + && name instanceof Var var && !isVariable.test(var.getName()))) + return Optional.empty(); + Expression argument = invocation.getArgs().get(0); + Optional> ofType = setsFor.apply(argument); + List sets = states.stream().map(GhostState::getParent).filter(Objects::nonNull).distinct() + .filter(s -> s.matches(invocation.getName()) && ofType.map(p -> p.test(s)).orElse(true)).toList(); + long withState = sets.stream().filter(s -> !statesOf(s, var.getName()).isEmpty()).count(); + if (withState > 0 && (ofType.isPresent() || withState == sets.size())) + return Optional.of(new FunctionInvocation(qualifiedLike(invocation.getName(), var.getName()), + List.of(argument.clone()))); + if (withState == 0) + for (GhostFunction s : sets) + if (isStateOfAnotherSet(var.getName(), s)) + throw new CustomError(String.format("State '%s' is not a state of '%s' (its states are %s)", + var.getName(), s.getName(), + statesOf(s, null).stream().map(GhostState::getName).collect(Collectors.joining(", ")))); + return Optional.empty(); + } + + /** The states of {@code set}, or only those named {@code name} when it is not null */ + private List statesOf(GhostFunction set, String name) { + return states.stream().filter(s -> s.getParent() == set && (name == null || s.getName().equals(name))).toList(); + } + + /** {@code state} qualified as {@code setName} is: {@code a.B.phase} gives {@code a.B.open} */ + private static String qualifiedLike(String setName, String state) { + int dot = setName.lastIndexOf('.'); + return dot < 0 ? state : setName.substring(0, dot + 1) + state; + } + + private boolean isStateOfAnotherSet(String name, GhostFunction stateSet) { + return states.stream().anyMatch(s -> s.getName().equals(name) && s.getParent() != null + && s.getParent() != stateSet && s.getParent().getPrefix().equals(stateSet.getPrefix())); + } +} 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 459f460d..ec988afd 100644 --- a/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestStateHints.java +++ b/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestStateHints.java @@ -347,6 +347,13 @@ void foundKeepsANamedStateSetByItsName() { error.getMessage().replaceAll("[⁰¹²³⁴⁵⁶⁷⁸⁹]", "")); } + @Test + void queryWrittenWithItsStateSetIsOfferedAsAGuard() { + assertHints("ErrorStateValueQuery.java", + new Hint(Kind.NEEDED_STATE, "The state of d is unknown here, and this call needs it to be unlocked"), + new Hint(Kind.GUARD, "Guard this call with if (d.isUnlocked()): when it returns true, d is unlocked")); + } + @Test void classWithoutStateSetKeepsTheGeneralHint() { assertHints("ErrorUnconstrainedStateRefinement.java", Hint.general(