/netspec

Primary LanguageScala

Synthesizing Formal Network Specifications from Input-Output Examples

Software requirements

Install souffle 2.0.1 and sbt following these instructions.

  1. souffle 2.0.1.
  2. sbt.

Run all benchmarks in paper

Benchmarks are listed in benchmarks. Files in each benchmakrs are explained here.

Synthesize a program:

sbt run learn <path to benchmark directory>

Synthesize with active learning:

  1. Prepare an oracle Datalog program in the benchmark directory, named -sol.dl, which answers the query questions. See an example.
  2. Run command: sbt run active <path to benchmark directory>