# Trace2Model

**Repository Path**: voidwu/Trace2Model

## Basic Information

- **Project Name**: Trace2Model
- **Description**: No description available
- **Primary Language**: Unknown
- **License**: BSD-3-Clause
- **Default Branch**: master
- **Homepage**: None
- **GVP Project**: No

## Statistics

- **Stars**: 0
- **Forks**: 0
- **Created**: 2020-09-08
- **Last Updated**: 2020-12-19

## Categories & Tags

**Categories**: Uncategorized

**Tags**: None

## README

# Trace2Model
A framework to learn system models from system execution traces. <br/>
Based on work presented in 'Learning Concise Models from Long Execution Traces' (https://arxiv.org/abs/2001.05230)

## Usage
`python3 <module_file_name> [args]`<br/>
Use the `-h` option to see module arguments.

The modules available in this framework are divided into two categories:
1. Automata learning modules - generate automata from given trace input <br/>
  a. Incremental NFA learning: `incr.py` <br/>
  b. DFA learning: `dfa.py` <br/>
2. Transition expression synthesis modules - generate a sequence of transition predicates from raw trace data, to be used as input to automata learning modules in 1. <br/>
  a. Synthesize expressions that will serve as transition conditions for next event: `syn_next_event.py` <br/>
  b. Synthesize expressions that will serve as transition predicates for data update across transitions: `syn_event_update.py` <br/>

For the synthesis modules 2a and 2b, a new trace file `<input_filename>_events.txt` is created with a sequence of transition predicates. Use this as input to the model learning modules 1a and 1b.

Use the `-h` option to see module arguments. You can use `run.py` to run a set of benchmarks already present in the tool. See the `benchmarks` folder.

## Tool Dependencies
You'll need the following tools installed (installation instructions for Fedora 29, Ubuntu 18.04 and MacOS 10.15 are provided below):
1. `CVC4 v1.6`: https://cvc4.github.io/downloads.html
2. `CBMC v5.10`: https://www.cprover.org/cbmc/
3. `Fastsynth` : https://github.com/kroening/fastsynth
4. `z3 v4.7.1` : https://github.com/Z3Prover/z3

## Benchmarks
There are a few trace files already provided to play around with the tool in the `benchmarks` folder
1. `dfa_bench` : benchmarks for non-incremental DFA learning
2. `incr_bench` : benchmarks for incremental NFA learning
3. `syn_bench` : benchmarks for predicate synthesis

## Setup Instructions

### Fedora (tested for Fedora 29)

1. Install Basic Requirements
~~~
  dnf -y groupinstall "Development Tools"
  dnf -y install kernel-devel kernel-headers
  dnf -y install gcc gcc-c++ flex bison perl-libwww-perl patch git
~~~

2. Install Tool Dependencies
~~~
  dnf -y install python3 cvc4 z3
~~~

Building Fastsynth
~~~
  git clone https://github.com/kroening/fastsynth.git
  cd fastsynth
  git reset --hard b8841e05ef97a35d28fb097fa0e19cc998021997
  git submodule init
  git submodule update
  cd lib/cbmc
  make -C src minisat2-download
  make -C src
  export PATH=$PATH:$(pwd)/src/cbmc
  cd ../../src
  make
  cd fastsynth
  export PATH=$PATH:$(pwd)
~~~

3. Python Modules
~~~
  dnf -y install graphviz graphviz-devel pkg-config python3-devel redhat-rpm-config
  pip3 install numpy pygraphviz transitions termcolor
~~~

4. Clone the repository `Trace2Model`<br/>
~~~
  git clone https://github.com/natasha-jeppu/Trace2Model.git Trace2Model
~~~
Check Fastsynth installation : 
~~~
  cd Trace2Model
  fastsynth ./aux_files/simplify_event.sl
  fastsynth ./aux_files/gen_event_update.sl
~~~


### Ubuntu 18.04

1. Install Basic Requirements
~~~
  apt-get -y install build-essential
  apt-get -y install g++ gcc flex bison make git libwww-perl patch
~~~

2. Install Tool Dependencies
~~~
  apt-get -y install python3 cvc4 cbmc z3
~~~

Building Fastsynth
~~~
  git clone https://github.com/kroening/fastsynth.git
  cd fastsynth
  git reset --hard b8841e05ef97a35d28fb097fa0e19cc998021997
  git submodule init
  git submodule update
  cd lib/cbmc
  make -C src minisat2-download
  make -C src
  cd ../../src
  make
  cd fastsynth
  export PATH=$PATH:$(pwd)
~~~

3. Python Modules
~~~
  apt-get -y install graphviz libgraphviz-dev pkg-config python3-pip python3-setuptools
  pip3 install numpy pygraphviz transitions termcolor
~~~

4. Clone the repository `Trace2Model`<br/>
~~~
  git clone https://github.com/natasha-jeppu/Trace2Model.git Trace2Model
~~~
Check Fastsynth installation : 
~~~
  cd Trace2Model
  fastsynth ./aux_files/simplify_event.sl
  fastsynth ./aux_files/gen_event_update.sl
~~~




### MacOS (tested on MacOS 10.15)
You will need Homebrew for installation. You can install it from https://brew.sh. <br/>
1. Python Modules
~~~
  brew install python3
  brew install graphviz
  pip3 install numpy transitions termcolor
~~~
  Include graphviz PATH for pygraphviz installation as shown below:
~~~
  pip3 install pygraphviz --install-option="--include-path=/usr/local/Cellar/graphviz/2.44.0/include/graphviz" --install-option="--library-path=/usr/local/Cellar/graphviz/2.44.0/lib"
~~~

2. Install Tool Dependencies
~~~
  brew tap cvc4/cvc4
  brew install cvc4/cvc4/cvc4
  brew install z3
~~~

  Building Fastsynth<br/>
  Install Xcode 10.x for Fastsynth build
~~~
  git clone https://github.com/kroening/fastsynth.git
  cd fastsynth
  git reset --hard b8841e05ef97a35d28fb097fa0e19cc998021997
  git submodule init
  git submodule update
  cd lib/cbmc
  make -C src minisat2-download
  make -C src
  export PATH=$PATH:$(pwd)/src/cbmc
  cd ../../src
  make
  cd fastsynth
  export PATH=$PATH:$(pwd)
~~~


3. Clone the repository `Trace2Model`<br/>
~~~
  git clone https://github.com/natasha-jeppu/Trace2Model.git Trace2Model
~~~
  Check Fastsynth installation :
~~~
  cd Trace2Model
  fastsynth ./aux_files/simplify_event.sl
  fastsynth ./aux_files/gen_event_update.sl
~~~