Convert an Ivy transition system (after its liveness-to-safety reduction) to a mypyvy input file, as a first step towards applying invariant inference.
To get an input file suitable for ivy-to-mypyvy, run ivy_check l2s_debug=true mutex.ivy > l2s.out.
Run with cargo run -- l2s.out. Currently for the mutex and better_mutex examples the
required cleanup is the following:
cargo run -- tests/mutex.l2s.out | sed -e 's/\?/thread/g' -e '2aimmutable constant t0: thread' > mutex.pyv
cargo run -- tests/better_mutex.l2s.out | sed -e 's/\?/thread/g' -e '2aimmutable constant t0: thread' > better_mutex.pyvFor ticket.ivy, we start with the example in the Ivy repo, then manually
simplify it (removing fancy Ivy features) to
ticket.ivy.
There is still some manual work which is more involved than above, so it's
wrapped up in a script: Run ./scripts/ticket.sh > ticket.pyv to generate that
file.
The ticket example is tricky to support because in Ivy it uses actions with
return values, and after manually implementing that it's still tricky because
the liveness-to-safety reduction uses relations l2s_d and l2s_a over
arbitrary values rather than values from just one of the two sorts (thread and
ticket). In the other examples there's only one sort so this isn't an issue.
You can then verify the liveness property using the hand-written invariants, for example:
mypyvy verify mutex.pyv
mypyvy verify better_mutex.pyv
mypyvy verify ticket.pyv(I have an alias for mypyvy, without that you'd pass the path to
mypyvy.sh.)
For debugging purposes, cargo run -- --ivy tests/mutex.l2s.out will parse and then print
back the Ivy input.
We use cargo-insta for snapshot testing, which records the expected output in a file. This helps monitor changes in the output while automatically managing the output.
Install with cargo install cargo-insta and then run cargo insta test --review, which will prompt to accept changes if the output has changed. The
tests still run as usual with cargo test.
The Ivy grammar is written using rust-peg as an embedded DSL in
ivy_l2s.rs. The grammar is a PEG
grammar. PEGs are pretty cool. You can debug
the parser using pegviz; after
installing the pegviz tool, run cargo run --release --features trace -- tests/l2s.out | pegviz --output pegviz.html and then look at the generated
pegviz.html file. On the Rust side this just traces the grammar, and then
outside the trace is visualized into a parse trace.