search

reactive-systems / syfco

Synthesis Format Conversion Tool
MIT License
23 stars 12 forks source link

Moore interpretation rejected as not in GR(1) #18

Open johnyf opened 8 years ago

johnyf commented 8 years ago

The following input to syfco -f slugsin file.tlsf:

INFO {
  TITLE:       "debugging example"
  DESCRIPTION: "debugging example"
  SEMANTICS:   Moore
  TARGET:      Mealy
}

MAIN {
  INPUTS { x; }
  OUTPUTS { y; }
  GUARANTEES { G ( F (x -> y)) }
}

yields:

"Conversion Error": not in GR(1)
The given specification is not in GR(1), which is neccessary to convert to the slugsin format.

whereas, changing the header information to:

SEMANTICS:   Mealy

translates it. The formula is in the GR(1) fragment, independently of what the players take as input, so it seems that this should translate in both cases.