The parameter -os Mealy,Strict is ignored

[5nizza]

According to https://arxiv.org/pdf/1604.02284.pdf Section 3.2, the parameter -os Mealy,Strict when coinciding with SEMANTICS should produce the authentic GR1 formula, not a formula with the global implication. The tool doesn't. Here is an example:

$ cat tmp.tlsf 
INFO {
  TITLE:       ""
  DESCRIPTION: "Exposition of bug"
  SEMANTICS:   Mealy,Strict
  TARGET:      Mealy
}

GLOBAL {
  PARAMETERS { }
  DEFINITIONS { }
}

MAIN {
  INPUTS { a; b; }
  OUTPUTS { c; d; }

  // env, sys init
  INITIALLY { a; b; }
  PRESET { c; d; }

  // env, sys safety
  REQUIRE { c -> (X a || X b); }
  ASSERT { a -> (X c && X d); }

  // env, sys GF
  ASSUME { G F !a; }
  GUARANTEE { G F d; }
}

Now run:

$ syfco ./tmp.tlsf -f ltl -m fully -os Mealy,Strict 
(((a) && (b)) -> (((c) && (d)) && (((G ((c) -> ((X (a)) || (X (b))))) && (G (F (! (a))))) -> ((G ((a) -> ((X (c)) && (X (d))))) && (G (F (d)))))))

It uses the global-implication semantics instead of weak until. Related to #25.

[ssardina]

I can confirm that, and add that it does produce the strict version with weak until when -os Mealy alone is used:

It also seems that the SEMANTICS section in the TLSF file is ignored, always produces the non-strict standard semantics.

[ssardina]

@5nizza , no news on this right? Have you found a way around?

[5nizza]

@ssardina nope, in my context, I had to manually encode it into the right semantics.

[ssardina]

Ouch! What a pity...

See that, against all intuitions, the strict semantics is obtained if you use -os Mealy!

[5nizza]

@ssardina oh, thanks for noticing, I use this hack now.