reactive-systems / syfco

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

`syfco` hangs on this simple spec that uses a recursive definition #50

Closed 5nizza closed 1 year ago

5nizza commented 1 year ago

Consider the simple spec:

INFO {
  TITLE:       ""
  DESCRIPTION: ""
  SEMANTICS:   Mealy
  TARGET:      Mealy
}

GLOBAL {
  DEFINITIONS {
    bf(i) =
      i < 1 : true
      bf(0);
  }
}

MAIN {
  INPUTS {
    r;
  }

  OUTPUTS {
    g;
  }

  GUARANTEES {
    bf(0);
  }
}

It is equivalent to true. When converting this spec using syfco -f basic (or any other format), syfco hangs. Strange. Any ideas? On spec simple_arbiter that also uses the recursive definition, syfco performs fine.

5nizza commented 1 year ago

argh, my mistake: used the syntax incorrectly, the definition of bf(i) should be something like:

 bf(i) =
      i < 1 : true
      otherwise: bf(0);