whitemech / lydia Goto Github PK
View Code? Open in Web Editor NEWA tool for LDLf translation to DFA and for LDLf synthesis.
License: GNU Lesser General Public License v3.0
A tool for LDLf translation to DFA and for LDLf synthesis.
License: GNU Lesser General Public License v3.0
See Section 5 of SPOT manual
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
.
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.
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
.
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.
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
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
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.
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.
Is your feature request related to a problem? Please describe.
Describe the solution you'd like
Describe alternatives you've considered
Additional context
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.
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:
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
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
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
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
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
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++
Describe the solution you'd like
Prevent adding a transition to Symbolic DFA from state 0, because it is the default sink.
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
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.
Describe the solution you'd like
Instead of evaluating the delta function, leave it symbolic and compute all the possible NFA successors.
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:
whitemech/lydia:0.1.0
: docker pull whitemech/lydia:0.1.0
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):
0.1.0
Additional context
n/a
A declarative, efficient, and flexible JavaScript library for building user interfaces.
🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
An Open Source Machine Learning Framework for Everyone
The Web framework for perfectionists with deadlines.
A PHP framework for web artisans
Bring data to life with SVG, Canvas and HTML. 📊📈🎉
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
Some thing interesting about web. New door for the world.
A server is a program made to process requests and deliver data to clients.
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
Some thing interesting about visualization, use data art
Some thing interesting about game, make everyone happy.
We are working to build community through open source technology. NB: members must have two-factor auth.
Open source projects and samples from Microsoft.
Google ❤️ Open Source for everyone.
Alibaba Open Source for everyone
Data-Driven Documents codes.
China tencent open source team.