Skip to content

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!"
Clone this wiki locally