Skip to content

Commit b9683e9

Browse files
CatarinaGamboaclaude
CatarinaGamboa
and
claude
committed
Count only checks of the receiver, and keep joins out of the checked case
- A state mentioned through another value counts as a check only when it is applied to the receiver's instance or to an object the solver proves equal to it. A check of another object leaves the state unknown. What the error shows as found is only computed when needed. - A join of every state across several state sets is no longer taken for a check, so it keeps the "No sequence of calls" hint. - Name the receiver's states in every state set the call checks, so a join that differs in a checked set still lists each state. - When every state allows the call, each by its own state refinement, name the needed state per refinement. - Search the smallest cover exactly up to 13 candidate groups. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
1 parent d01610c commit b9683e9

17 files changed

Lines changed: 433 additions & 51 deletions

File tree

‎liquidjava-example/src/main/java/testSuite/ErrorStateHintJoinOneOfTwoSets.java‎

Lines changed: 29 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,29 @@
1+
package testSuite;
2+
3+
import liquidjava.specification.StateRefinement;
4+
import liquidjava.specification.StateSet;
5+
6+
// The paths differ in one of two state sets, so the states are named in both sets the call checks
7+
@StateSet({"closed", "opened"})
8+
@StateSet({"unlocked", "locked"})
9+
public class ErrorStateHintJoinOneOfTwoSets {
10+
11+
@StateRefinement(to = "closed(this) && unlocked(this)")
12+
public ErrorStateHintJoinOneOfTwoSets() {}
13+
14+
@StateRefinement(from = "closed(this)", to = "opened(this)")
15+
public void open() {}
16+
17+
@StateRefinement(from = "unlocked(this)", to = "locked(this)")
18+
public void lock() {}
19+
20+
@StateRefinement(from = "closed(this) && unlocked(this)")
21+
public void enter() {}
22+
23+
public static void use(boolean p) {
24+
ErrorStateHintJoinOneOfTwoSets d = new ErrorStateHintJoinOneOfTwoSets();
25+
if (p)
26+
d.open();
27+
d.enter(); // Expect: State Refinement Error
28+
}
29+
}

‎liquidjava-example/src/main/java/testSuite/ErrorStateHintJoinTwoSets.java‎

Lines changed: 31 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,31 @@
1+
package testSuite;
2+
3+
import liquidjava.specification.StateRefinement;
4+
import liquidjava.specification.StateSet;
5+
6+
// Every combination of two state sets is reached on some path: a join of every state, not a lack of knowledge
7+
@StateSet({"closed", "opened"})
8+
@StateSet({"unlocked", "locked"})
9+
public class ErrorStateHintJoinTwoSets {
10+
11+
@StateRefinement(to = "closed(this) && unlocked(this)")
12+
public ErrorStateHintJoinTwoSets() {}
13+
14+
@StateRefinement(from = "closed(this)", to = "opened(this)")
15+
public void open() {}
16+
17+
@StateRefinement(from = "unlocked(this)", to = "locked(this)")
18+
public void lock() {}
19+
20+
@StateRefinement(from = "closed(this) && unlocked(this)")
21+
public void enter() {}
22+
23+
public static void use(boolean p, boolean q) {
24+
ErrorStateHintJoinTwoSets d = new ErrorStateHintJoinTwoSets();
25+
if (p)
26+
d.open();
27+
if (q)
28+
d.lock();
29+
d.enter(); // Expect: State Refinement Error
30+
}
31+
}

‎liquidjava-example/src/main/java/testSuite/ErrorStateHintUnknownToggleTwoSets.java‎

Lines changed: 21 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,21 @@
1+
package testSuite;
2+
3+
import liquidjava.specification.StateRefinement;
4+
import liquidjava.specification.StateSet;
5+
6+
// Every state allows flip(), by the refinement for a or the one for b, so the hint names a or b, not all six states
7+
@StateSet({"a", "b"})
8+
@StateSet({"x", "y", "z"})
9+
public class ErrorStateHintUnknownToggleTwoSets {
10+
11+
@StateRefinement(to = "a(this) && x(this)")
12+
public ErrorStateHintUnknownToggleTwoSets() {}
13+
14+
@StateRefinement(from = "a(this)", to = "b(this)")
15+
@StateRefinement(from = "b(this)", to = "a(this)")
16+
public void flip() {}
17+
18+
public static void use(ErrorStateHintUnknownToggleTwoSets t) {
19+
t.flip(); // Expect: State Refinement Error
20+
}
21+
}

‎liquidjava-example/src/main/java/testSuite/classes/state_hint_checked_copy_error/Reader.java‎

Lines changed: 14 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,14 @@
1+
package testSuite.classes.state_hint_checked_copy_error;
2+
3+
import java.util.Scanner;
4+
5+
// The failed check is on it and the call on a variable holding the same scanner, so the state was checked
6+
public class Reader {
7+
8+
public static void nextOfTheSameScanner(Scanner it) {
9+
Scanner same = it;
10+
if (!it.hasNext()) {
11+
same.next(); // Expect: State Refinement Error
12+
}
13+
}
14+
}

‎liquidjava-example/src/main/java/testSuite/classes/state_hint_checked_copy_error/ScannerRefinements.java‎

Lines changed: 17 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,17 @@
1+
package testSuite.classes.state_hint_checked_copy_error;
2+
3+
import liquidjava.specification.ExternalRefinementsFor;
4+
import liquidjava.specification.Refinement;
5+
import liquidjava.specification.StateRefinement;
6+
import liquidjava.specification.StateSet;
7+
8+
@StateSet({"hasMore", "noMore"})
9+
@ExternalRefinementsFor("java.util.Scanner")
10+
public interface ScannerRefinements {
11+
12+
@Refinement("_ == true --> hasMore(this)")
13+
boolean hasNext();
14+
15+
@StateRefinement(from = "hasMore(this)", to = "noMore(this)")
16+
String next();
17+
}

‎liquidjava-example/src/main/java/testSuite/classes/state_hint_checked_other_object_error/Reader.java‎

Lines changed: 13 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,13 @@
1+
package testSuite.classes.state_hint_checked_other_object_error;
2+
3+
import java.util.Scanner;
4+
5+
// Another scanner was checked, so nothing is known about the state of the receiver
6+
public class Reader {
7+
8+
public static void nextOfTheOther(Scanner other, Scanner it) {
9+
if (other.hasNext()) {
10+
it.next(); // Expect: State Refinement Error
11+
}
12+
}
13+
}

‎liquidjava-example/src/main/java/testSuite/classes/state_hint_checked_other_object_error/ScannerRefinements.java‎

Lines changed: 17 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,17 @@
1+
package testSuite.classes.state_hint_checked_other_object_error;
2+
3+
import liquidjava.specification.ExternalRefinementsFor;
4+
import liquidjava.specification.Refinement;
5+
import liquidjava.specification.StateRefinement;
6+
import liquidjava.specification.StateSet;
7+
8+
@StateSet({"hasMore", "noMore"})
9+
@ExternalRefinementsFor("java.util.Scanner")
10+
public interface ScannerRefinements {
11+
12+
@Refinement("_ == true --> hasMore(this)")
13+
boolean hasNext();
14+
15+
@StateRefinement(from = "hasMore(this)", to = "noMore(this)")
16+
String next();
17+
}

‎liquidjava-example/src/main/java/testSuite/classes/state_hint_checked_wrong_object_error/Reader.java‎

Lines changed: 13 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,13 @@
1+
package testSuite.classes.state_hint_checked_wrong_object_error;
2+
3+
import java.util.Scanner;
4+
5+
// The check is on it, but the call is on another scanner, whose state is unknown
6+
public class Reader {
7+
8+
public static void checkedTheWrongObject(Scanner it, Scanner other) {
9+
if (it.hasNext()) {
10+
other.next(); // Expect: State Refinement Error
11+
}
12+
}
13+
}

‎liquidjava-example/src/main/java/testSuite/classes/state_hint_checked_wrong_object_error/ScannerRefinements.java‎

Lines changed: 17 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,17 @@
1+
package testSuite.classes.state_hint_checked_wrong_object_error;
2+
3+
import liquidjava.specification.ExternalRefinementsFor;
4+
import liquidjava.specification.Refinement;
5+
import liquidjava.specification.StateRefinement;
6+
import liquidjava.specification.StateSet;
7+
8+
@StateSet({"hasMore", "noMore"})
9+
@ExternalRefinementsFor("java.util.Scanner")
10+
public interface ScannerRefinements {
11+
12+
@Refinement("_ == true --> hasMore(this)")
13+
boolean hasNext();
14+
15+
@StateRefinement(from = "hasMore(this)", to = "noMore(this)")
16+
String next();
17+
}

‎liquidjava-verifier/src/main/java/liquidjava/diagnostics/hints/StateHints.java‎

Lines changed: 50 additions & 22 deletions
Original file line numberDiff line numberDiff line change
@@ -5,6 +5,7 @@
55
import java.util.List;
66
import java.util.Optional;
77
import java.util.Set;
8+
import java.util.TreeSet;
89
import java.util.function.Supplier;
910
import java.util.stream.Collectors;
1011
import java.util.stream.Stream;
@@ -34,10 +35,17 @@ public final class StateHints {
3435

3536
private final StateMachine machine;
3637
private final String receiver;
38+
/** The states that allow the failing call, grouped by the state refinement that allows it */
39+
private final List<Set<State>> goals;
40+
/** The state sets the failing call checks, as indexes into {@link State#names()} */
41+
private final Set<Integer> checked;
3742

38-
private StateHints(StateMachine machine, String receiver) {
43+
private StateHints(StateMachine machine, String receiver, RefinedFunction call) {
3944
this.machine = machine;
4045
this.receiver = receiver;
46+
this.goals = machine.statesAllowingByRefinement(call);
47+
this.checked = goals.stream().flatMap(g -> machine.stateSetsNamed(g).stream())
48+
.collect(Collectors.toCollection(TreeSet::new));
4149
}
4250

4351
/**
@@ -49,23 +57,24 @@ private StateHints(StateMachine machine, String receiver) {
4957
* the receiver as written in the code
5058
* @param category
5159
* the error's category, or {@code null} if it has none
60+
* @param checked
61+
* whether the receiver's state was checked elsewhere, though not decided, e.g. by an earlier call whose
62+
* result says which state it is in
5263
*/
5364
public static List<Hint> forCall(StateMachine machine, RefinedFunction call, Set<State> current, String receiver,
54-
ErrorCategory category) {
65+
ErrorCategory category, boolean checked) {
5566
if (!machine.models(call) || current.isEmpty() || machine.allows(current, call))
5667
return List.of(); // the machine cannot explain why the call failed
5768
Set<State> goal = machine.statesAllowing(call);
5869
if (goal.isEmpty())
5970
return List.of();
6071

61-
StateHints hints = new StateHints(machine, receiver);
62-
if (category == ErrorCategory.UNKNOWN)
63-
return hints.anyState(current, call, goal, false);
64-
if (category == null && current.size() == machine.states().size())
65-
return hints.anyState(current, call, goal, true); // something is known, e.g. an earlier check failed
72+
StateHints hints = new StateHints(machine, receiver, call);
73+
if (category == ErrorCategory.UNKNOWN || checked)
74+
return hints.anyState(current, call, checked);
6675
boolean pathDependent = category == ErrorCategory.PATH_DEPENDENT_STATE;
67-
List<Hint> sequences = hints.howToReach(current, call, hints.names(current),
68-
() -> machine.complete() ? List.of(hints.unreachable(current, call, goal, pathDependent)) : List.of());
76+
List<Hint> sequences = hints.howToReach(current, call, hints.namesHere(current),
77+
() -> machine.complete() ? List.of(hints.unreachable(current, call, pathDependent)) : List.of());
6978
return Stream.concat(sequences.stream(), hints.allowedCalls(current).stream()).toList();
7079
}
7180

@@ -86,13 +95,13 @@ public static Hint decidingArgument(DecidingArgument deciding, String receiver)
8695
* A call allowed in only some states is never suggested, since whether it is allowed is just as unknown. Calls that
8796
* only tell which state the object is in are not in the machine, so no hint suggests checking one first.
8897
*
89-
* @param somethingKnown
90-
* whether anything is known about the state, though not enough to rule out any state
98+
* @param checked
99+
* whether the state was checked, though the check did not decide it
91100
*/
92-
private List<Hint> anyState(Set<State> current, RefinedFunction call, Set<State> goal, boolean somethingKnown) {
93-
String known = somethingKnown ? "What is known here does not decide the state of " + receiver
101+
private List<Hint> anyState(Set<State> current, RefinedFunction call, boolean checked) {
102+
String known = checked ? "What is known here does not decide the state of " + receiver
94103
: "The state of " + receiver + " is unknown here";
95-
String message = known + ", and this call needs it to be " + names(goal);
104+
String message = known + ", and this call needs it to be " + needed();
96105
message += newObjects(call).map(c -> ". Objects created with " + c + " start in such a state").orElse("");
97106
List<Hint> hints = new ArrayList<>();
98107
hints.add(new Hint(Kind.NEEDED_STATE, message));
@@ -130,14 +139,14 @@ private Hint callSequence(Set<State> current, List<RefinedFunction> sequence, St
130139
receiver, from, names(reached)));
131140
}
132141

133-
private Hint unreachable(Set<State> current, RefinedFunction call, Set<State> goal, boolean pathDependent) {
142+
private Hint unreachable(Set<State> current, RefinedFunction call, boolean pathDependent) {
134143
if (pathDependent)
135144
return new Hint(Kind.PATH_DEPENDENT_STATE, String.format(
136145
"%s can be in %s here, depending on the path taken, and no sequence of calls moves all of them to %s. "
137146
+ "Make %s reach this line in the same state on every path",
138-
receiver, names(current), names(goal), receiver));
139-
String message = String.format("No sequence of calls moves %s from %s to %s", receiver, names(current),
140-
names(goal));
147+
receiver, namesHere(current), needed(), receiver));
148+
String message = String.format("No sequence of calls moves %s from %s to %s", receiver, namesHere(current),
149+
needed());
141150
message += newObjects(call).map(c -> ". Create a new object instead with " + c).orElse("");
142151
return new Hint(Kind.UNREACHABLE_STATE, message);
143152
}
@@ -148,13 +157,13 @@ private List<Hint> allowedCalls(Set<State> current) {
148157
List<String> signatures = allowed.stream().map(StateHints::signature).toList();
149158
String others = machine.complete() ? "" : " (and possibly others)";
150159
return List.of(new Hint(Kind.AVAILABLE_CALLS, String.format("In state %s, %s can call: %s%s",
151-
names(current), receiver, list(signatures), others)));
160+
namesHere(current), receiver, list(signatures), others)));
152161
}
153162
boolean noCallsInAnyState = current.stream().allMatch(s -> machine.allowedIn(Set.of(s)).isEmpty());
154163
if (machine.complete() && noCallsInAnyState)
155164
return List.of(new Hint(Kind.FINAL_STATE,
156165
String.format("%s is in state %s, where none of its methods with state refinements can be called",
157-
receiver, names(current))));
166+
receiver, namesHere(current))));
158167
return List.of();
159168
}
160169

@@ -186,8 +195,27 @@ private static String parameters(RefinedFunction function) {
186195

187196
/** {@code states} named as briefly as possible, e.g. {@code open or loud} */
188197
private String names(Collection<State> states) {
189-
return machine.describe(states).stream().map(group -> String.join(" and ", group))
190-
.collect(Collectors.joining(" or "));
198+
return names(machine.describe(states));
199+
}
200+
201+
/** The states the receiver can be in, named in the state sets the call checks and any set they all agree on */
202+
private String namesHere(Collection<State> current) {
203+
return names(machine.describe(current, checked));
204+
}
205+
206+
/**
207+
* The states that allow the call. If every state does, each by a different state refinement, the states each
208+
* refinement allows are named on their own: {@code a or b}, not every state.
209+
*/
210+
private String needed() {
211+
Set<State> goal = machine.ordered(goals.stream().flatMap(Set::stream).toList());
212+
if (goal.size() < machine.states().size())
213+
return names(goal);
214+
return goals.stream().map(this::names).distinct().collect(Collectors.joining(" or "));
215+
}
216+
217+
private static String names(List<List<String>> groups) {
218+
return groups.stream().map(group -> String.join(" and ", group)).collect(Collectors.joining(" or "));
191219
}
192220

193221
private static String list(List<String> items) {

0 commit comments

Comments
 (0)