|
7 | 7 | import java.util.Set; |
8 | 8 | import java.util.TreeSet; |
9 | 9 | import java.util.function.Supplier; |
10 | | -import java.util.function.UnaryOperator; |
| 10 | +import java.util.function.Function; |
11 | 11 | import java.util.stream.Collectors; |
12 | 12 | import java.util.stream.Stream; |
13 | 13 |
|
@@ -42,12 +42,21 @@ public final class StateHints { |
42 | 42 | private final List<Set<State>> goals; |
43 | 43 | /** The state sets the failing call checks, as indexes into {@link State#names()} */ |
44 | 44 | private final Set<Integer> checkedSets; |
45 | | - private final UnaryOperator<String> stateName; |
| 45 | + /** The name of the state set a state is shown as a value of, or empty when it keeps the shorthand */ |
| 46 | + private final Function<String, Optional<String>> setNameOf; |
| 47 | + /** |
| 48 | + * Whether states are shown as the error's message shows them, e.g. {@code lockState(d) == locked}: when some state |
| 49 | + * set of the class is shown by its name |
| 50 | + */ |
| 51 | + private final boolean asValues; |
46 | 52 |
|
47 | | - private StateHints(StateMachine machine, String receiver, RefinedFunction call, UnaryOperator<String> stateName) { |
| 53 | + private StateHints(StateMachine machine, String receiver, RefinedFunction call, |
| 54 | + Function<String, Optional<String>> setNameOf) { |
48 | 55 | this.machine = machine; |
49 | 56 | this.receiver = receiver; |
50 | | - this.stateName = stateName; |
| 57 | + this.setNameOf = setNameOf; |
| 58 | + this.asValues = machine.states().stream().flatMap(s -> s.names().stream()) |
| 59 | + .anyMatch(name -> setNameOf.apply(name).isPresent()); |
51 | 60 | this.goals = machine.statesAllowingByRefinement(call); |
52 | 61 | this.checkedSets = goals.stream().flatMap(g -> machine.stateSetsNamed(g).stream()) |
53 | 62 | .collect(Collectors.toCollection(TreeSet::new)); |
@@ -65,14 +74,15 @@ private StateHints(StateMachine machine, String receiver, RefinedFunction call, |
65 | 74 | * @param checkedElsewhere |
66 | 75 | * whether the receiver's state was checked elsewhere, though not decided, e.g. by an earlier call whose |
67 | 76 | * result says which state it is in |
68 | | - * @param stateName |
69 | | - * a state's name as the error shows it, e.g. {@code lockState == locked} for {@code locked} |
| 77 | + * @param setNameOf |
| 78 | + * the name of the state set the error's message shows a state as a value of, or empty when it shows the |
| 79 | + * shorthand |
70 | 80 | */ |
71 | 81 | public static List<Hint> forCall(StateMachine machine, RefinedFunction call, Set<State> current, String receiver, |
72 | | - ErrorCategory category, boolean checkedElsewhere, UnaryOperator<String> stateName) { |
| 82 | + ErrorCategory category, boolean checkedElsewhere, Function<String, Optional<String>> setNameOf) { |
73 | 83 | if (!machine.models(call) || current.isEmpty() || machine.allows(current, call)) |
74 | 84 | return List.of(); // the machine cannot explain why the call failed |
75 | | - StateHints hints = new StateHints(machine, receiver, call, stateName); |
| 85 | + StateHints hints = new StateHints(machine, receiver, call, setNameOf); |
76 | 86 | if (hints.goals.isEmpty()) |
77 | 87 | return List.of(); |
78 | 88 |
|
@@ -112,7 +122,7 @@ public static Hint decidingArgument(DecidingArgument deciding, String receiver) |
112 | 122 | private List<Hint> anyState(Set<State> current, RefinedFunction call, boolean checkedElsewhere) { |
113 | 123 | String known = checkedElsewhere ? "What is known here does not decide the state of " + receiver |
114 | 124 | : "The state of " + receiver + " is unknown here"; |
115 | | - String message = known + ", and this call needs it to be " + needed(); |
| 125 | + String message = known + ", and this call needs " + (asValues ? "" : "it to be ") + needed(); |
116 | 126 | message += newObjects(call).map(c -> ". Objects created with " + c + " start in such a state").orElse(""); |
117 | 127 | List<Hint> hints = new ArrayList<>(); |
118 | 128 | hints.add(new Hint(Kind.NEEDED_STATE, message)); |
@@ -166,8 +176,8 @@ private List<Hint> guard(Set<State> current, RefinedFunction call) { |
166 | 176 | String check = (negated ? "!" : "") + guardCall(guard.method()); |
167 | 177 | String arguments = guard.method().getArguments().isEmpty() ? "" |
168 | 178 | : ", filling in the arguments of " + declaration(guard.method()); |
169 | | - String message = String.format("Guard this call with if (%s)%s: when it returns %s, %s is %s", check, arguments, |
170 | | - !negated, receiver, needed()); |
| 179 | + String message = String.format("Guard this call with if (%s)%s: when it returns %s, %s", check, arguments, |
| 180 | + !negated, (asValues ? "" : receiver + " is ") + needed()); |
171 | 181 | return List.of(new Hint(Kind.GUARD, message)); |
172 | 182 | } |
173 | 183 |
|
@@ -211,6 +221,11 @@ private Hint callSequence(Set<State> current, List<CallVariant> sequence, boolea |
211 | 221 | } |
212 | 222 |
|
213 | 223 | private Hint unreachable(Set<State> current, RefinedFunction call, boolean pathDependent) { |
| 224 | + if (pathDependent && asValues) |
| 225 | + return new Hint(Kind.PATH_DEPENDENT_STATE, String.format( |
| 226 | + "Depending on the path taken, %s here, and no sequence of calls moves %s from all of them to %s. " |
| 227 | + + "Make %s reach this line in the same state on every path", |
| 228 | + namesHere(current), receiver, needed(), receiver)); |
214 | 229 | if (pathDependent) |
215 | 230 | return new Hint(Kind.PATH_DEPENDENT_STATE, String.format( |
216 | 231 | "%s can be in %s here, depending on the path taken, and no sequence of calls moves all of them to %s. " |
@@ -227,13 +242,15 @@ private List<Hint> allowedCalls(Set<State> current) { |
227 | 242 | if (!allowed.isEmpty()) { |
228 | 243 | List<String> signatures = allowed.stream().map(StateHints::signature).toList(); |
229 | 244 | String others = machine.complete() ? "" : " (and possibly others)"; |
230 | | - return List.of(new Hint(Kind.AVAILABLE_CALLS, String.format("In state %s, %s can call: %s%s", |
231 | | - namesHere(current), receiver, list(signatures), others))); |
| 245 | + return List.of(new Hint(Kind.AVAILABLE_CALLS, String.format("%s %s, %s can call: %s%s", |
| 246 | + asValues ? "When" : "In state", namesHere(current), receiver, list(signatures), others))); |
232 | 247 | } |
233 | 248 | boolean noCallsInAnyState = current.stream().allMatch(s -> machine.allowedIn(Set.of(s)).isEmpty()); |
234 | 249 | if (machine.complete() && noCallsInAnyState) |
235 | | - return List.of(new Hint(Kind.FINAL_STATE, |
236 | | - String.format("%s is in state %s, where none of its methods with state refinements can be called", |
| 250 | + return List.of(new Hint(Kind.FINAL_STATE, asValues |
| 251 | + ? String.format("When %s, none of the methods of %s with state refinements can be called", |
| 252 | + namesHere(current), receiver) |
| 253 | + : String.format("%s is in state %s, where none of its methods with state refinements can be called", |
237 | 254 | receiver, namesHere(current)))); |
238 | 255 | return List.of(); |
239 | 256 | } |
@@ -322,11 +339,22 @@ private String needed() { |
322 | 339 | /** The groups joined by {@code or}, each in parentheses if it has several states and there are other groups */ |
323 | 340 | private String join(List<List<String>> groups) { |
324 | 341 | return groups.stream().map(group -> { |
325 | | - String states = group.stream().map(stateName).collect(Collectors.joining(" and ")); |
| 342 | + String states = group.stream().map(this::stateName).collect(Collectors.joining(" and ")); |
326 | 343 | return groups.size() > 1 && group.size() > 1 ? "(" + states + ")" : states; |
327 | 344 | }).collect(Collectors.joining(" or ")); |
328 | 345 | } |
329 | 346 |
|
| 347 | + /** |
| 348 | + * A state as the error's message shows it, e.g. {@code lockState(d) == locked}, or {@code closed(d)} for a state |
| 349 | + * that keeps the shorthand, or only its name if no state set of the class is shown by its name |
| 350 | + */ |
| 351 | + private String stateName(String state) { |
| 352 | + if (!asValues) |
| 353 | + return state; |
| 354 | + return setNameOf.apply(state).map(set -> set + "(" + receiver + ") == " + state) |
| 355 | + .orElse(state + "(" + receiver + ")"); |
| 356 | + } |
| 357 | + |
330 | 358 | private static String list(List<String> items) { |
331 | 359 | if (items.size() <= MAX_LISTED_CALLS) |
332 | 360 | return String.join(", ", items); |
|