Improving forward generation by "inlining" -- experiments and design doc - #58
Open
mwhicks1 wants to merge 3 commits into
Open
Improving forward generation by "inlining" -- experiments and design doc#58mwhicks1 wants to merge 3 commits into
mwhicks1 wants to merge 3 commits into
Conversation
Adds the design write-up (Docs/Lookahead-experiment.md) for generating command
sequences with hard-to-satisfy preconditions via adjacent-step inlining, plus a
companion note on steering (Docs/Steering-notes.md) and an appendix explaining
why the state-machine/path-planning framing is the wrong one (control and data
cannot be separated).
Includes the hand-written experiments the design is based on:
* perfect-square ticket vault (flat Step/Trace): baseline, fused pair,
all-combinations;
* guarded-dereference (self-recursive typing relation over a tree): baseline,
fused, all-combinations (inlining across the typing relation and the
membership relation it calls).
No changes to Specimen itself; experiments are self-contained and build.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Consider a state-transition specification — a step relation whose constructors are the labeled edges of a state machine, plus a trace relation that chains steps:
Suppose we ask Specimen to derive a forward generator for
Trace: from a start state it walks the machine, at each step picking an enabled edge, which it adds to the trace. Unfortunately, when aCmdhas a precondition that isn't cheaply satisfiable, the forward generator often fails to exercise that command. This PR includes a pair of design documents about ways to fix this problem, backed up by experiments also committed. A key insight is that inStepwe might want to "inline" multiple steps into a single branch, so that a generation decision in oneCmdcan be influenced by a precondition on a downstreamCmd. Follow-on PRs explore implementation of this design.By submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice.