Comments (4)
I agree with Alexandre, that the current situation is a flaw and I would prefer to have the dual conditions to be defined as duals. So I suggest to define generalized-Streett
as dual to generalized-Rabin
. One reason for that is the consistency of the notation for the number of accepting sets, i.e. 3 2 1 0
from acc-name: generalized-Streett 3 2 1 0
. For generalized-Rabin
we have that the numbers 2 1 0
specify the numbers of sets in the second components of the pairs.
How painful would it be to change the definition of Streett
?
(Btw. generalized-Streett 3 0 0 0
should be equivalent to generalized-Buchi 3
. The one we would like to agree to Streett 3
is generalized-Streett 3 1 1 1
.)
from hoaf.
I also vote for the second option: generalized-Streett 3 2 1 0
should stand for
Acceptance: 6 (Inf(0)|Fin(1)|Fin(2))&(Inf(3)|Fin(4))&Inf(5)
. Further, I suggest to change the definition of Streett
accordingly.
The question is when to fix the definition of Streett
. I see two options:
- Consider the current state as a bug and fix it immediately.
- Fix it at the next major release (2.0).
The second option is politically (more) correct, but it could also bring more damage. I think that now the option Streett
is used by very few third-party tools (or maybe none), but if we wait with the fix until the next major release, more tools may start to use the buggy version of Streett
. Hence I vote for the first option.
from hoaf.
I'm voting to change this now too.
Currently the Spot's autfilt --generalized-streett
generates the first form (i.e., the generalization of the "flawed" Streett), but does not output acc-name: generalized-streett
. I don't think anybody is using this option, so I'm not afraid to reorder the generalized Streett acceptance.
Regarding Streett, at least ltl2dstar
is one producer of Streett automata that would need to be changed. Spot can read those and has some dedicated Streett->TGBA conversion algorithm that currently only detect Streett acceptance if it is given as in the HOA spec. I'd be happy to adjust this algorithm to support both style of Streett acceptance (I'll need to support both style anyway if Spot has to read/write both versions of the format).
from hoaf.
To make some progress, I've merged the Alexandre's pull request #66 (we all agreed on) and corrected the bugs detected by Joachim (
I'm almost sure that the option with two alternative names for Streett acceptance (with different order of Fins and Infs) would not get serious support.
What remains to be decided is the new version number: Do we want to switch to v2 or release it as v1.1?
I have no strong opinion here: I tend to slightly prefer v1.1 as the changes are not very big. On the other hand, the current description of version numbers says:
The major version number should be updated in case of changes that invalidate the syntax or semantic of earlier versions.
I'm afraid that this is a strong reason to switch to v2 (or change the description of version number semantics such that the changes of header entries starting with lowercase is not the reason to change major version number).
from hoaf.
Related Issues (20)
- better wording in case States: is not given HOT 8
- better encoding for parity acceptance HOT 6
- constraints between acc-name and Acceptance HOT 6
- on the semantics of parity acceptance HOT 10
- the definition of F as a set of sets sounds incorrect HOT 2
- HOA logo HOT 9
- add "semi-deterministic" property HOT 25
- Support for non-AP alphabets HOT 4
- Add Alphabet header for specifying an alphabet not based on atomic propositions HOT 6
- Properties: Add syntactic support (or convention) for negation of properties HOT 5
- Formalize the semantics of the version number HOT 19
- Edges or transitions? HOT 4
- ε-labelled transitions HOT 13
- fixing the semantic of the deterministic property HOT 1
- Figures referenced from examples in README.md are not working HOT 2
- transition-based acceptance marks in alternating automata HOT 3
- Not clear whether acceptance sets can be specified both on a set and some of its exit arcs HOT 3
- No clear way to specify dead-end states HOT 1
- add "controllable-AP" header
Recommend Projects
-
React
A declarative, efficient, and flexible JavaScript library for building user interfaces.
-
Vue.js
🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
-
Typescript
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
-
TensorFlow
An Open Source Machine Learning Framework for Everyone
-
Django
The Web framework for perfectionists with deadlines.
-
Laravel
A PHP framework for web artisans
-
D3
Bring data to life with SVG, Canvas and HTML. 📊📈🎉
-
Recommend Topics
-
javascript
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
-
web
Some thing interesting about web. New door for the world.
-
server
A server is a program made to process requests and deliver data to clients.
-
Machine learning
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
-
Visualization
Some thing interesting about visualization, use data art
-
Game
Some thing interesting about game, make everyone happy.
Recommend Org
-
Facebook
We are working to build community through open source technology. NB: members must have two-factor auth.
-
Microsoft
Open source projects and samples from Microsoft.
-
Google
Google ❤️ Open Source for everyone.
-
Alibaba
Alibaba Open Source for everyone
-
D3
Data-Driven Documents codes.
-
Tencent
China tencent open source team.
from hoaf.