-
Notifications
You must be signed in to change notification settings - Fork 13
Open
Description
Consider the following specification.
$ cat gr1_bug.tlsf
INFO {
TITLE: ""
DESCRIPTION: ""
SEMANTICS: Mealy
TARGET: Mealy
}
GLOBAL {
PARAMETERS { }
DEFINITIONS { }
}
MAIN {
INPUTS { r; }
OUTPUTS { g; }
INITIALLY { }
PRESET { }
REQUIRE { }
ASSERT { g; }
ASSUME { G F r; }
GUARANTEE { }
}
It is clearly a GR(1) spec. However, the tool claims it is not.
$ syfco ./gr1_bug.tlsf -gr
NOT in the Generalized Reactivity fragment: ./gr1_bug.tlsf
As a result, it cannot be converted into slugs format:
$ syfco ./gr1_bug.tlsf -f slugs
"Conversion Error": not in GR(1)
The given specification is not in GR(1), which is neccessary to convert to the slugs format.
Metadata
Metadata
Assignees
Labels
No labels