Metadata-Version: 2.1
Name: ltlcross_wrapper
Version: 0.6.1
Summary: Python wrapper around tool ltlcross from Spot library
Home-page: https://github.com/xblahoud/ltlcross_wrapper
Author: Fanda Blahoudek
Author-email: fandikb+dev@gmail.com
License: MIT
Description: # ltlcross wrapper
        Python wrapper around the amazing tool `ltlcross` from [Spot](https://spot.lrde.epita.fr/) library.
        The tool compares LTL to automata translators.
        
        ## Requires
        * [Spot](https://spot.lrde.epita.fr/)
        * Python >= 3.6
        
        The following libraries are needed for bokeh scatter plots (can be used in Jupyter)
        * [bokeh](https://bokeh.org/) (installs automatically by `pip`)
        * [colorcet](https://colorcet.holoviz.org/) (installs automatically by `pip`)
        * [jupyter_bokeh](https://github.com/bokeh/jupyter_bokeh) for rendering the plots in JupyterLab
        
        ## Installation
        ```
        python3 -m pip install -U ltlcross_wrapper
        ```
        
        ## Usage
        ltlcross_wrapper offers 2 classes:
         * `Modulizer`splits a big `ltlcross` task into smaller ones, execute the small
            tasks in parallel, and merge the intermediate results into one final `.csv`, `.log`,
            and `_bogus.ltl` files.
         * `ResAnalyzer` parses the results of `ltlcross`, and implements several functions
            to analyze and visualize the results, mainly in Jupyter notebooks. 
        
        ### Modulizer
        We need to specify the tools and file(s) with formulas which ltlcross should 
        use. The tools are given as a dict whose items are pairs `(name, ltlcross_cmd)` 
        where `ltlcross_cmd` is `COMMANDFMT` from `man ltlcross`.
         
            tools = {"LTL3HOA"    : "ltl3hoa -d -x -i -p 2 -f %f > %O",
                     "SPOT"       : "ltl2tgba"
                    }
        
        Typical usage of `Modulizer` follows.
        
            m = Modulizer(tools, formulas.ltl)
            mp.run()
         
         The above command splits the file `formulas.ltl` into several files with
         2 formulas each, and uses 4 processes to run ltlcross on these small files
         in parallel. The number of processes can be controlled by setting 
         `processes` in both the constructor and the function `run()`. The number
         of formulas in each small file can be changed by setting `chunk_size`
         in the constructor.
         
         If a previous computation was interrupted for some reason, consider using
            
            m.resume()
         instead of `m.run()`. The function `m.resume()` will skip computing the
         small tasks for which it already finds an `.csv` file with the result.
         
         You can delete the final results and intermediate files, and rerun the
         computation by
         
            m.recompute()
            
        By default, all intermediate files will be created in directory 
        `modular.parts` and the merged files `modular.csv`, `modular.log`,
        `modular_bogus.ltl` will be created in the current directory. The base
        `modular` can be changed to `new_name` simply by setting `name=new_name`.
        Otherwise, each filename/dirname can be changed by setting `out_res_file`, 
        `out_log_file`, `out_bogus_file`, and `tmp_dir`.
        
        TODO: Explain ltlcross options
        
        ### Results' Analyzer
        
        See the [usage notebook](Usage.ipynb). Currently, bokeh scatter plots do not
        render directly on github so you might consider to [see the notebook on nbviewer](https://nbviewer.jupyter.org/github/xblahoud/ltlcross_wrapper/blob/master/Usage.ipynb)
        
Platform: UNKNOWN
Classifier: License :: OSI Approved :: MIT License
Classifier: Programming Language :: Python :: 3
Classifier: Programming Language :: Python :: 3.6
Requires-Python: >=3.6.0
Description-Content-Type: text/markdown
