Skip to content

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

@johnyf

Description

@johnyf

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.

Metadata

Metadata

Assignees

No one assigned

    Labels

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions