Comments (4)
I still like this idea. Concrete proposals:
- language-properties: for language-based properties and properties: for automata properties
- With prefix: lang-stutter-invariant vs deterministic
- ...?
I have no strong opinions about the syntax. Besides stutter-invariant, what other language properties would we like to list? Ideas:
- safety: every rejected word has a bad prefix, i.e., a prefix w such that w w' is rejected for all infinite words w'
- liveness: for all finite words w, there is an accepted word w' with prefix w
- universal: language consists of all infinite words
- empty: language is empty
Alexandre, you do property classification in Spot, are there some classifications that we could use here?
from hoaf.
I prefer syntax 1.
from hoaf.
I don't like the prefixes, Joachim's number 1. is fine
from hoaf.
I was thinking about this after reading Joachim's email, and I think I'm simply fine with the current situation.
- we already have tools that, following the current wording of the specifications, build automata with language-dependent properties such as
properties: stutter-invariant
, and tools that consume it. E.g.,ltl2tgba
can outputproperties: stutter-invariant
and the development version ofltl2dstar
can use it. - for all specified properties, it is easy to tell whether they are language-dependent or not
- we have 0 experience with user-supplied properties
Splitting "properties:" into two headers just for the purpose of being able to handle unknown language properties if they are ever needed, seems to require some changes in our tools and in the format, for no immediate benefits. If you really want to do it, I'll do it as well of course, but my (lazy!) inclination would be not to work on this until we can actually feel it is needed.
Currently, if we want to preserve language-related properties in our tools, we need a hard-coded list of those properties. That is fine with me, as I already have to make explicit decisions in all algorithms about the other non-language-related properties I keep track of.
I also feel like those language properties is only a fraction of the problem. There might be non-language-related properties that are preserved by a transformation, and that tools do not know about. Again, I think we lack experience. If we ever have user-defined properties to preserve, an easy fix for our tools would be to have an option like --keep-prop=foo
allowing user to tell: "run your algorithm, but keep the foo property if it was present in the input because that is important to me". The same idea could be applied to unknown headers. Again, I'm not suggesting to implement those options: I'm just saying this is something we can easily do later if we do nothing now.
from hoaf.
Related Issues (20)
- 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
- generalized Streett? HOT 4
- 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
- Conversion to BA format? HOT 8
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.