whitemech/cynthia

SDD-based Forward LTLf Synthesis

cynthia's Issues

API to transform LTLf formulas in Negation Normal Form

Ideally, it should be implemented as a Visitor.

NNF for non-empty trace vs empty-trace semantics

This issue is to keep track of a discrepancy between NNF with empty-trace and non-empty trace semantics.

For example, let us denote ~ the logical not and ! the propositional not. Also, let a be an atom.

The NNF of a is a in both semantics.
The NNF of !a is !a in both semantics.
The NNF of ~a should be !a | end for empty-trace sem., and !a for non-empty trace sem.
The NNF of ~!a should be a | end for empty-trace sem., and a for non-empty trace sem.

Hamming distance heuristic

Is your feature request related to a problem? Please describe.
A clear and concise description of what the problem is. Ex. I'm always frustrated when [...]

Describe the solution you'd like
A clear and concise description of what you want to happen.

Describe alternatives you've considered
A clear and concise description of any alternative solutions or features you've considered.

Additional context
Add any other context or screenshots about the feature request here.

Formula progression

Partfile parser

This parser reads a partfile and stores the environment-agent variable partition.

Check full compliance with standard grammar

After #2, the library logic and parser allow to build the syntax tree of a formula from a textual description.
The grammar tries to comply with A Standard Grammar for Temporal Logics on Finite Traces, but the PR does not include operators like "weak until" W and "strong release" M.

The goal of this issue is to double-check that the full syntax is supported by our parser.