Metadata-Version: 2.1
Name: Scarlet-ltl
Version: 0.0.3
Summary: A package for learning LTL formulas from a sample consisting of traces partitioned into positive and negative
Author-email: Ritam Raha <ritam.raha18@gmail.com>, Rajarshi Roy <rajarshi008@gmail.com>, Nathanael Fijalkow <nathanael.fijalkow@gmail.com>, Daniel Neider <daniel.neider@uni-oldenburg.de>
License: Copyright (c) 2022 University of Antwerp, Belgium & LaBRI, University of Bordeaux, France
        		   Ritam Raha <ritam.raha18@gmail.com>
        
        Permission is hereby granted, free of charge, to any person obtaining
        a copy of this software and associated documentation files (the
        "Software"), to deal in the Software without restriction, including
        without limitation the rights to use, copy, modify, merge, publish,
        distribute, sublicense, and/or sell copies of the Software, and to
        permit persons to whom the Software is furnished to do so, subject to
        the following conditions:
        
        The above copyright notice and this permission notice shall be
        included in all copies or substantial portions of the Software.
        
        THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,
        EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF
        MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
        NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE
        LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION
        OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION
        WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
        
Project-URL: Homepage, https://github.com/rajarshi008/Scarlet
Project-URL: Paper, https://link.springer.com/chapter/10.1007/978-3-030-99524-9_14
Classifier: Programming Language :: Python :: 3
Classifier: License :: OSI Approved :: MIT License
Classifier: Operating System :: OS Independent
Requires-Python: >=3.7
Description-Content-Type: text/markdown
Requires-Dist: lark
Requires-Dist: graphviz
Requires-Dist: ltlf2dfa

<h1 align="center">
  <img src="https://rajarshi008.github.io/assets/images/scarlet-logo.png" width="60%">
 </h1>


---
## SCARLET 


We solve the problem of learning LTL formulas from a sample consisting of traces partitioned into positive and negative.
A [paper](https://link.springer.com/chapter/10.1007/978-3-030-99524-9_14) 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](https://www.brics.dk/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


