-
Notifications
You must be signed in to change notification settings - Fork 42
Kore REPL Sample Interaction Idea #2
Vladimir Ciobanu edited this page Mar 19, 2019
·
1 revision
Left: Input and output
Right: Commentary
Kore> step 100
-- After a long time...
^C
Stopped after 17 step(s) due to user interrupt
Kore> config
...
-- Notice a huge predicate in the configuration
-- making everything unreadable
Kore> simplification-start-config
...
-- Notice that the configuration seems reasonable.
Kore> reset-simplification
Kore> reduce 1 -- Simplify by applying 1 rewrite rules.
Done.
Kore> config
... -- Nothing suspicious.
Kore> reduce 2 -- Simplify by applying 2 rewrite rules.
Done.
Kore> config
... -- Nothing suspicious.
Kore> reduce 4 -- Simplify by applying 4 rewrite rules.
Done.
Kore> config
... -- Nothing suspicious.
Kore> reduce 8 -- Simplify by applying 8 rewrite rules.
Kore> config
... -- Signs of large predicate.
Kore> reset-simplification
Kore> reduce 8 -- Simplify by applying 8 rewrite rules.
...
-- Continue binary search
-- "Oh, now I understand what happens!"