whitemech/lydia

A tool for LDLf translation to DFA and for LDLf synthesis.

lydia's Issues

Symbolic delta function

Describe the solution you'd like
Instead of evaluating the delta function, leave it symbolic and compute all the possible NFA successors.

Do synthesis with strategy

Formula simplification

See Section 5 of SPOT manual

https://spot.lrde.epita.fr/tl.pdf

Add copyright notice check

Is your feature request related to a problem? Please describe.
Currently, we don't check that every file has the copyright notice.

Describe the solution you'd like
Add a CI script that does that check.

Describe alternatives you've considered
N/A

Additional context
N/A

`lydia --version` does not work

Describe the bug
Using lydia --version does not work; it prints:

--logic is required
Run with --help for more information.

To Reproduce
Steps to reproduce the behavior:

1. Pull the Docker image whitemech/lydia:0.1.0: docker pull whitemech/lydia:0.1.0
2. Run docker run -it whitemech/lydia lydia --version

Expected behavior
Lydia prints the version of the tool: 0.1.0

Screenshots

n/a

Desktop (please complete the following information):

• OS: Ubuntu 20.04
• Lydia version 0.1.0

Additional context
n/a

Add API documentation

Is your feature request related to a problem? Please describe.
Currently, we don't use any docs generator from code.

Describe the solution you'd like
Use such documentation (e.g. Doxygen).

Describe alternatives you've considered
N/A

Additional context
N/A

Use enable_shared_from_this

Investigate whether the usage of std::enable_shared_from_this can help in our library.

One of the pain points is that we have to forbid static allocation. However, that would let us in many parts of the library to take the shared pointer of the current instance instead of creating a new one.

From Symbolic DFA to HOA

Is your feature request related to a problem? Please describe.
It is missing a proper way to represent an automaton in a specific format. HOA format seems to be a pretty standard approach for that: http://adl.github.io/hoaf/

Describe the solution you'd like
Support conversion from DFA to HOA.

Describe alternatives you've considered

Additional context

Add Clang Tidy checks

Is your feature request related to a problem? Please describe.

Currently, we don't have checks for code style.

Describe the solution you'd like

Add Clang Tidy checks.

Describe alternatives you've considered

Additional context

Update dev Docker images for Mac

Is your feature request related to a problem? Please describe.

Describe the solution you'd like

Describe alternatives you've considered

Additional context

Prevent changing the state 0 of a DFA.

Is your feature request related to a problem? Please describe.

When the DFA is built incrementally, the library should prevent any change to the state 0, that is:

• cannot be set as a final state
• cannot add a transition from it

Notice: transitions to state 0 are already present by default, because the BDDs for each bit only store the transitions that lead to positive bits.

Describe the solution you'd like
n/a

Describe alternatives you've considered
n/a

Additional context
n/a

Don't link MONA GTA Library

Currently, the MONA GTA library is linked to the liblydia.a library. Such dependency is not actually needed to compile the Lydia library, and therefore should be removed.

Thanks to @Shufang-Zhu that reported the problem, as in its platform the building gives an error regarding the linking to libmonagta.so.

Support all regular expressions

Is your feature request related to a problem? Please describe.

Code support for all regular expressions is missing.

Describe the solution you'd like

Implement all the regular expressions.

Describe alternatives you've considered

Additional context

Prevent add transition to Symbolic DFA from state 0

Describe the solution you'd like
Prevent adding a transition to Symbolic DFA from state 0, because it is the default sink.

Minimal model algorithm for `to_dfa`

• literature review on minimal model algorithms

base.cpp:82:16: error: ‘invalid_argument’ is not a member of ‘std’

Trying to build Lydia on Ubuntu 21.04, gcc 10.3.0

lydia/lib/src/logic/ltlf/base.cpp:82:16: error: ‘invalid_argument’ is not a member of ‘std’ 82 | throw std::invalid_argument("LTLfAnd formula: arguments must be > 1"); | ^~~~~~~~~~~~~~~~

Adding #include <stdexcept> to base.cpp would fix the bug.

Implement Parser in Flex/Bison

Update installation instructions for MacOS users

It seems we need the following variable updates for OSX installation:

export PATH="/usr/local/opt/bison/bin:$PATH"                                    
export PATH="/usr/local/opt/flex/bin:$PATH"
export CPLUS_INCLUDE_PATH=/System/Volumes/Data/usr/local/Cellar/flex/2.6.4_1/include/:$CPLUS_INCLUDE_PATH
export CXX=/usr/bin/clang++

Reintroduce minimal models algorithm

The minimal model algorithm implementation (QuickXPlain) has been temporarily removed to avoid to block the development. It became obsolete after #72, since we are migrating to use Minisat rather than Cryptominisat.

However, it could be useful to have it back. This issue is just to keep in mind that. The old implementation can be recovered from the commits of the linked PR.

Add code coverage checks

Is your feature request related to a problem? Please describe.

Currently, we don't have checks for the code coverage (e.g. Codecov).

Describe the solution you'd like

Add step for code coverage in CI.

Describe alternatives you've considered
N/A

Additional context
N/A

Support all LDLf regular expressions

Comparison with MONA

Is your feature request related to a problem? Please describe.
It is not clear what are the performances of Lydia compared to successful tools like MONA.

Describe the solution you'd like
Provide a comparison, and populate some sections of the documentation accordingly.

Benchmark analysis

parser optimization

Is your feature request related to a problem? Please describe.
Formulas are naively parsed so that the built AST is not the one naturally expected. Instead, it's unbalanced. E.g., the formula <a;b;c>tt will be parsed as <a;(b;c)>tt, therefore creating as AST as:

    ;
a       ;
     b    c

Describe the solution you'd like
We'd like the AST to be as:

     ;
a    b    c 

Describe alternatives you've considered
There are two alternatives. The first one is to simplify the AST while building the AST. The second one is to have the parser taking care of it. Unfortunately, bison does not allow for it.
For now, we will simplify the AST at code level. In the future, we might consider changing the parser with ANTLR.

something wrong with the demo "examples/counter_1.ltlf" in README

Describe the bug
i run this demo in 'readme.md':

/lydia$ lydia -l ltlf -f examples/counter_1.ltlf --part examples/counter_1.part
[2022-01-10 21:39:19.438] [lydia] [info] [main] Parsing "examples/counter_1.ltlf"
COError: syntax error at 1.5
Parse failed!

maybe somethig wrong in the "examples/counter_1.ltlf", and how can I fix it?

---

By the way, maybe it can add some suggestions for installation, for me, I add this into "CMakeList.txt" can help.

# cudd
set (CUDD_LIBRARIES /home/tridu33/cudd/lib/libcudd.a)
set (CUDD_INCLUDE_DIRS /home/tridu33/cudd/include)
set (MONA_INCLUDE_DIRS /usr/include/mona)
# for 'cppitertools',in bash i  do this:
#  "export CPLUS_INCLUDE_PATH=/mnt/host/d/ltlsynthesis/lydia/third_party/cppitertools:$CPLUS_INCLUDE_PATH"
message(">>> SET DEFAULT TO BEFORE, include_dirs=${dirs}")

---

also, when i built Syft+, after make install,

$ ls /usr/local/bin
Syft  ltlf2fol  lydia

when i call "Syft --help" , it shows that "./ltlf2fol NOT FOUND", then i need to do this:
change this:

string LTLF2FOL = "./ltlf2fol NNF "+LTLFfile+" >"+FOL;

to this:

string LTLF2FOL = "ltlf2fol NNF "+LTLFfile+" >"+FOL;

in line 8 of syft\src\synthesis\main.cpp.

Boolean operations on Symbolic DFAs

Use off-the-shelf minimal model algorithm to compute next NFA state.

Is your feature request related to a problem? Please describe.

Currently, there's no smart computation of minimal models after the delta function is returned.

Describe the solution you'd like
Use some off-the-shelf library, or implement your own, algorithm to compute minimal models of a propositional formula.

Describe alternatives you've considered

Additional context

Refactor automatic translation of LDLf in LTLf in LTLfParser

The current behaviour of LTLfParser is to directly translate LTLf formulae into LDLf formulae.

This is not ideal in general, especially for programmatic usage. It conflates two concepts, parsing and translation, into one class. Would be better to have a separate visitor class that does the translation from LTLf to LDLf.