Repository navigation
Open
Labels
enhancementNew feature or requestNew feature or request
Description
Once we have hints for the possible fixes of the path, we can try to show them on the state machine view, where a user can select one of the hints and we show it on the state machine highlighted (maybe in yellow, with dashes and with an animation of the dashes moving so we see it's like a possibility but not a fixed path).
Where this stands
- The State Machine view lists the verifier's hints of the shown error in a Ways to fix section (Show the verifier's hints in the State Machine view #172, for Collapse what does not help when focusing the state machine on an error, and show the ways to fix it #170).
- Paths read from the diagram alone were tried in Collapse the unrelated methods when focusing on a state error, listed on hover #171 and dropped: they ignore the transitions' conditions and the code. So a path drawn here should come from the verifier's hints.
What is left for this issue
Selecting a verifier hint and drawing that path, animated, on the diagram. Before this is possible:
- Structured hints:
HintDTOis only(kind, message). The verifier would need to send the calls of a call-sequence hint and the states it goes through, not just text, so the view never has to parse messages. - Mapping states: the hints are computed on the verifier's
StateMachineBuilder, whose states are combinations of every@StateSet. The diagrams show one machine per state set (Show one state machine diagram per state set #163), so each combination must be projected onto the right diagram. - Incompleteness: when the machine is incomplete, the hints end with "(and possibly others)". The drawn path must read as one possibility, which is what the animated dashes are for.
- The study: hints can give the answer away. Like the hints in the Verification tab, this stays opt-in, behind a click.
Metadata
Metadata
Assignees
Labels
enhancementNew feature or requestNew feature or request
Activity