A package for learning LTL formulas from a sample consisting of traces partitioned into positive and negative
Project description
SCARLET
We solve the problem of learning LTL formulas from a sample consisting of traces partitioned into positive and negative.
A paper presenting the algorithms behind Scarlet
was published in TACAS'2022.
Installation
Installing the tool
Now, you can install the tool, as python package using pip command as follows:
python3 -m pip install Scarlet-ltl
Input File format:
The input files consist of traces separated as positives and negatives, separated by ---
.
Each trace is a sequence of letter separated by ;
. Each letter represents the truth value of atomic propositions.
An example of a trace is 1,0,1;0,0,0
which consists of two letters each of which define the values of three propositions (which by default consider to be p,q,r
). An example sample looks like the following:
0,0,0;0,1,1;1,0,0;0,0,1;0,1,0
1,1,0;1,0,1;1,0,0;1,1,1;1,0,1
1,1,0;0,1,1;1,1,1;1,0,0;1,0,1
---
1,0,0;1,0,0;0,1,0;1,1,0;1,1,1
1,0,0;1,0,0;0,1,0;1,1,0;1,0,0
0,0,1;1,0,0;1,1,0;1,1,1;1,0,0
How to run Scarlet:
Create input file
To run Scarlet, you have to create an input file with .trace
extension in the same directory where venv
folder is located. The input file format is described in the above section.
Run Scarlet on a particular input file
from Scarlet.ltllearner import LTLlearner
learner = LTLlearner(input_file = "input_file_name.trace")
learner.learn()
This will run Scarlet on the input trace file.
Parameters
You can call the LTLlearner
class with additional parameters as follows:
- input_file = the path of the file containing LTL formuas, i.e.,
= 'input_file_name.trace'
- timeout = For specifying the timeout,
default = 900
- csvname = the name of the output csv file, i.e.,
= 'output_file_name.csv'
- thres = the bound on loss function for noisy data,
default = 0
for perfect classification, has to be a number between zero and one
How to generate trace files from LTL formulas
You can also generate trace files from given LTL formulas following the instructions below:
Install dependencies
For generating benchmarks from a given set of LTL formula, we rely on a python package LTLf2DFA that uses MONA in its backend. As a result, one needs to install MONA first in order to be able to use this procedure (instructions can be found in the MONA website).
Create input formula file
For generating benchmarks, you have to create an input file named formulas.txt
in the same directory where venv
folder is located. The formula file should contain a list of formulas (in prefix notation) along with the alphabet.
An example of this file is as follows:
G(!(p));p
->(F(q), U(!(p),q));p,q
G(->(q, G(!(p))));p,q
Generate trace files from formulas.txt
from Scarlet.genBenchmarks import SampleGenerator
generator = SampleGenerator(formula_file= "formulas.txt")
generator.generate()
Parameters
You can call the SampleGenerator
class with additional parameters as follows:
- formula_file = the path of the file containing LTL formuas,
example = 'formulas.txt'
- sample_sizes = list of sample_size, i.e., number of positive traces and number of negative traces (separated by comma) in each sample,
default = [(10,10),(50,50)]
- trace_lengths = For specifying the length range for each trace in the samples,
default = [(6,6)]
- output_folder = For specifying the name of the folder in which samples are generated
Project details
Download files
Download the file for your platform. If you're not sure which to choose, learn more about installing packages.
Source Distribution
Built Distribution
Hashes for Scarlet_ltl-0.0.4-py3-none-any.whl
Algorithm | Hash digest | |
---|---|---|
SHA256 | cf1d522c02a4bb3a66e1df0a3aba285a79f843c400e6de2bef223feb3e5230c3 |
|
MD5 | 066f2bd423ca5a4b044519c298f6b12d |
|
BLAKE2b-256 | 3a68d57e229c2ad9296e36383ad5755b2628147d24c7b7fb5e865b02a45cf29c |