sebdisdv / ltlfuc Goto Github PK

View Code? Open in Web Editor NEW

Shell 0.01% C++ 2.90% Python 0.78% Perl 0.14% C 82.38% Emacs Lisp 0.75% Common Lisp 0.04% Awk 0.02% CSS 0.01% TeX 3.20% Makefile 0.25% HTML 7.24% PostScript 0.89% CMake 0.55% Batchfile 0.04% Yacc 0.44% Lex 0.03% M4 0.07% Roff 0.25%

ltlfuc's Introduction

Realizability check for pure Past Linear Temporal Logic on finite traces

Setup Environment

Python libraries

The python libraries necessary to run the main script can be installed in a virtual environment with the following command

pip install -r requirements.txt

Other tools for comparison

The following three tools needs to be installed on your machine along with their dependancies

Build NuSMV

For building NuSMV run the following commands

cd NuSMV
mkdir build && cd build
cmake ..
make

Create .env file

Once every tool is properly installed you need to create an .env file with the following five variables

NUSMV_EXEC_PATH = "<path_to>/NuSMV/build/bin/NuSMV"
NIKE_APP_PATH = "<path_to>/Nike/nike/build/apps/nike-app/nike-app"
SYFTMAX_EXEC_PATH = "<path_to>/SyftMax/build/bin/Syftmax"
SYNTHETICO_EXEC_PATH = "<path_to>/synthetico/build/synth"
LTL2SMV_EXEC_PATH = "<path_to>/NuSMV/build/bin/ltl2smv"

Run the experiments

python3 Pltl2Nusmv/test_dataset.py [-h] -i INPUT [-k] [-m] [-s]

optional arguments:
  -h, --help            show this help message and exit
  -i INPUT, --input INPUT The path to the json file containing the formulas
  -k, --nike            enable nike
  -m, --syftmax         enable syftmax
  -s, --synthetico      enable synthetico

Recommend Projects