gr1c
gr1c copied to clipboard
tulip-control
a collection of tools for GR(1) synthesis and related activities
The most frequent criticism that I receive about gr1c is that building gr1c is difficult on macOS and Windows. This can be practically solved by providing users with ready-to-execute files...
For instance, be able to recognize [](A -> B) and convert it to an equivalent specification, possibly adding extra required "flag" variables. The conversion process should be automatic with details...
currently gcov provides for measuring test coverage. this issue is to facilitate access and interpretation of that data via a visualization tool, like [gcovr](https://gcovr.com/en/stable/guide.html).
For example, ``` a == ... b == ... a ... ``` where the defined symbols are not variables, but simply expressions to be reused throughout. Similar in purpose and...
The strategy in JSON format uses node names that are obtained from memory addresses. Thus, these are numbers and cannot be used as identifiers. E.g., that interferes with applying `JSON.parse`...
This should be possible, by: 1. `f == EnvInit => SysInit` 2. `g == \E y: f` 3. `\A`-enumerate `g` over `x` 4. `h ==` substitute each assignment `x` in...
`Cudd_init(..., maxMemory)` does **not** place any hard limit on maximum memory occupation. Instead, an explicit call to [`Cudd_SetMaxMemory`](https://github.com/johnyf/cudd/blob/80c9396b7efcb24c33868aeffb89a557af0dc356/cudd/cudd/cuddAPI.c#L4440) is needed, in order to limit the memory occupation. A search within...
Currently gr1c uses exit codes both to indicate errors (including unhandled signals, e.g., segmentation faults) and to report some results, e.g., realizability. This can cause confusion when other programs are...
Make gr1c compatible with [openpromela](https://github.com/johnyf/openpromela). This may involve nontrivial extensions to gr1c, in which case corresponding issues should be opened. Besides gr1c, achieving this may require upstream changes to openpromela,...
Bloem et al [1] describe a GR(1) winning set computation that has quadratic complexity in the number states by exploiting a method for evaluating fixpoint expressions [2]. Try implementing this...
Metadata
Owner
Metadata
a collection of tools for GR(1) synthesis and related activities