Symbolic execution for verification of stateful data planes made easy and fast.
- JDK 8 (in case a different one is used the ScalaZ3 jar needs to be rebuilt against this, different, JDK)
- sbt - The simple build tool for Scala projects
See setup.sh for a concrete setup script (it was tested on 64bit Ubuntu 12.04, 14.04 and 15.10).
Then from project root issue sbt sample.
There is also a Vagrantfile if you prefer this option. This also uses setup.sh for provisioning.
If you choose to use setup.sh (or Vagrantfile + setup.sh) you should only grab those files since this includes the cloning of the repo.
See src/main/scala/change/v2/runners/experiments/SEFLRunner.scala to start experimenting with SEFL. sbt sample will run that code.
Look at the description of the instructions method in src/main/scala/org/change/v2/Template.scala; try to understand what the instructions attatched to input port 0 do. Check src/main/resources/click_test_files/Template.click in order to get the complete picture.
From the project root issue sbt click which performs the symbolic execution of Template.click file.
You should find the output in template.output.
Play with the code, check the output. Loop.