Strict semantics not working?

[ssardina]

When I ran on a Mealy,Strict file it gives the same as Mealy when translating to LTL:

The only difference between the files is the semantics:

Moreover, if I try to override the semantics in the command (as in the example in the README), it gives error:

[ssardina@Thinkpad-X1 tlsf]$ syfco -f ltl --overwrite-semantics Strict,Mealy test-strict.tlsf 
ConvertError {convSourceValue = "Strict,Mealy", convSourceType = "String", convDestType = "Semantics", convErrorMessage = "Unknown semantics"}

Test files attached. Same LTL output for both.

tlsf.zip

Any clue?

[ssardina]

This is 3rd point in #34, just that there they are trying to translate to SMV, but "strict " seems to have no effect.

[kleinreact]

It is correct that syfco -f ltl test-strict.tlsf and syfco -f ltl test-nonstrict.tlsf produce the same output, since semantics are preserved in both cases during the translation. Hence, the output of syfco -f ltl test-strict.tlsf still needs to be interpreted under the strict semantics, while the output of syfco -f ltl test-nonstrict.tlsf does not.

The problem is that the ltl format does not support any semantic information, which is why both outputs appear to be the same. This is also one of the reasons, why the semantics definition is part of TLSF and, thus, also makes TLSF more expressive.

If you like to convert test-strict.tlsf to an LTL formula with standard semantics, the semantics need to be overwritten:

$ syfco -f ltl --overwrite-semantics mealy test-strict.tlsf
! i1 && ! i2 -> (o1 || o2 W ! i1 || ! i2) && (! o1 || ! o2) && (G (i1 && i2) && ! i1 && ! i2 -> ! o1 || ! o1)

Uppercase letters produced an error, if part of the --overwrite-semantics parameter, which now has been fixed with 0f0f6a6. This explains the produced error message. The order of Mealy and Strict still need to be according to the TLSF 1.1 paper.

[5nizza]

oh, man, that is so counter-intuitive for me. I thought syfco will automatically translate into the target semantics. That means: if a format doesn't distinguish assumptions/guarantees stuff, then syfco will create the formula semantically equivalent to what is meant in TLSF. For example, if TLSF says "Mealy,Strict", then syfco uses the semantics with W when translating into ltl, otherwise it creates the formula with Gs only.

Without this automatic translation, the user needs to do the following steps when translating into, say, format ltl:

1. check what is the target semantics used in TLSF, call it S
2. when calling syfco to translate into ltl, indicate --overwrite-semantics S

thanks.

[ssardina]

Thanks @kleinreact for your answer and fixing the issue with capitalization. I tried it and it works. And yes I should have used "Mealy,Strict" above.

Now, I am quite puzzled with the standard vs strict semantics. My understanding from the TLSF manual is that to get the GR(1)-type shape that uses W, it should be in STRICT semantics:

However, as your answer above states (and I tested it myself), I get that GR(1) LTL shape with the W if I overwrite it to be just Mealy, that is NOT strict.

So I get the GR(1) when it is NOT strict?

I want to understand what is happening here. The file test-strict.tlsf has this:

  SEMANTICS:   Mealy,Strict
  TARGET:      Mealy

So the file should be interpreted as Mealy & Strict, with the following interpretation:

But, but, I get that translation to LTL only if I overwrite the SEMANTICS to be just standard Mealy:

$ syfco -f ltl --overwrite-semantics mealy test-strict.tlsf
! i1 && ! i2 -> (o1 || o2 W ! i1 || ! i2) && (! o1 || ! o2) && (G (i1 && i2) && ! i1 && ! i2 -> ! o1 || ! o1)

I am 101% sure I am missing something here and I am not understanding what SEMANTICS means and the TLSF Section 3 on "Target and Semantics". Particularly when it says "If the semantics is Mealy,Strict or Moore,Strict, and the TARGET coincides with the semantics system model"

Concrete question: is using --overwrite-semantics equivalent to editing the file and changing the SEMANTICS value? That is, is the above --overwrite-semantics mealy the same as editing test-strict.tlsf and replacing SEMANTICS: Mealy,Strict with SEMANTICS: Mealy ?

[kleinreact]

@5nizza: The problem with automatically translating between strict and non-strict semantics is that most of the target formats do not fix the samantics with the specification format. Thus, it is up to the tool reading the format to decide whether the specification is interpreted under strict semantics, or not.

@ssardina: Consider that the marked formula of the TLSF paper denotes the equivalent representation in standard LTL for a formula with strict semantics. Hence, it is not the strict (or GR(1)) representation itself, but how the formula looks like, if being translated to standard LTL. This is also the reason for getting the corresponding output in case of overwriting the semantics with Mealy, which indeed is non-strict.

Regarding your concrete question: No, --overwrite-semantics mealy is not equivalent to editing the SEMANTICS value. The tool parameter requests a change of the semantic interpretation of the generated output, which usually requires rewriting the formulas of the specification as well in order to produce an equivalent output.

You can easily observe this for example by translating to the basic format, i.e.:

syfco -f basic --overwrite-semantics mealy test-strict.tlsf

[ssardina]

Thanks @kleinreact for your prompt reply and elaboration ! I am getting, but slowly I am afraid... :-)

@ssardina: Consider that the marked formula of the TLSF paper denotes the equivalent representation in standard LTL for a formula with strict semantics. Hence, it is not the strict (or GR(1)) representation itself, but how the formula looks like, if being translated to standard LTL. This is also the reason for getting the corresponding output in case of overwriting the semantics with Mealy, which indeed is non-strict.

So, if I set Mealy,Strict in the SEMANTICS key, it does not state that the TLSF file should be understood as the LTL formula for strict realizability (the one with the W)?

My understanding was that the TLSF spec (which is not per se a logical formula but a formatted spec) could be interpreted in 2 ways: standard or strict. And each would amount to a different shape of LTL formula.

Regarding your concrete question: No, --overwrite-semantics mealy is not equivalent to editing the SEMANTICS value. The tool parameter requests a change of the semantic interpretation of the generated output, which usually requires rewriting the formulas of the specification as well in order to produce an equivalent output.

You can easily observe this for example by translating to the basic format, i.e.:

syfco -f basic --overwrite-semantics mealy test-strict.tlsf

Indeed, I saw that. If I do that, it is more than just changing the SEMANTIC key, it changes the whole file. So would be be correct if I claim that the --overwrite-semantics S will transform the file to an equivalent representation but under the new semantics specified S? I can see that happening as the W modality is added to the PRESET part in the above command. So it gives the equivalent LTL formula under the non-strict shape that happens to achieve the original strict LTL?

But if so, I just don't understand why:

[ssardina@Thinkpad-X1 tlsf]$ syfco -f ltl test-strict.tlsf
! i1 && ! i2 -> (! o1 || ! o2) && (G (i1 && i2) && ! i1 && ! i2 -> G (o1 || o2) && (! o1 || ! o1))

does not give me the strict LTL shape, sicne test-strict.tlsf has the semantics spec as strict. :-(

[kleinreact]

So, if I set Mealy,Strict in the SEMANTICS key, it does not state that the TLSF file should be understood as the LTL formula for strict realizability (the one with the W)?

There are two possiblities:

1. An LTL formula without W, separated in intial conditions, assumptions and guarantees interpreted under strict semantics.
2. An LTL formula with potential W interpreted under standard semantics that does not require any separation in general.

Both can be used to describe the same specification setting. TLSF supports both of them, where Mealy,Strict indicates the first variant (1) and Mealy the second (2). Thus, you are correct: Mealy,Strict does not state that the TLSF file should be understood as an LTL formula with standard semantics (which is the one with W).

I claim that the --overwrite-semantics S will transform the file to an equivalent representation but under the new semantics specified S? I can see that happening as the W modality is added to the PRESET part in the above command. So it gives the equivalent LTL formula under the non-strict shape that happens to achieve the original strict LTL?

Both correct.

But if so, I just don't understand why:

[ssardina@Thinkpad-X1 tlsf]$ syfco -f ltl test-strict.tlsf ! i1 && ! i2 -> (! o1 || ! o2) && (G (i1 && i2) && ! i1 && ! i2 -> G (o1 || o2) && (! o1 || ! o1))

does not give me the strict LTL shape, sicne test-strict.tlsf has the semantics spec as strict. :-(

Your assumption is that the ltl format is always interpreted under standard LTL semantics, which causes the problem with your understanding. The point is, the ltl format just does not care about the chosen semantics, but only considers the formula, as it for example also does not consider the distinction between inputs and outputs. It may be a valid design decision to declare that the semantics are alwasy standard, if nothing else is stated. However, we decided against that, because there are other tools using the ltl format with strict semantic interpretation as well. As a consequence, it is the responsibility of the user of syfco to choose the correct transformation with respect to the surrounding toolchain.

[ssardina]

OK it is all making more sense, once again thanks for follow up this thread; I really want to get to the bottom of it. At least I got the meaning of the --overwrite-semantics option, so that is fully done! :-) But, I am either not understanding something key still (most probable) OR the TLSF paper is unclear/confusing in Section 3.2.

So, when I said "interpreted", I always meant the TLSF spec, not the LTL formula. As you said at the end of your last post, an LTL formula is just that, a formula, and the "way" to read the formula is given by the semantics of the logic, which is why the TLSF paper says in both cases "as the formula in standard LTL semantics". So first it seems to me that "standard semantics" is overloaded in that Section 3.2, as it could mean just the usual LTL semantics (well, I guess under the reactive LTL framework with input/output) OR the semantics ascribed to the TLSF specification as a type of LTL shape.

Now see that it says "The TLSF spec is interpreted as the LTL formula X in standard LTL semantics":

So, what I get from all that text is that which LTL formula the TLSF spec corresponds to depends on the value of SEMANTICS field:

1. If you have Mealy alone, it corresponds to the "standard" shape of LTL formula, that is, the one NOT using W and where we know there could be some counter-intutitive results (as the system can trivially satisfy the formula)
2. If you have Mealy,Strict, then the TLSF spec corresponds to the "strict" shape of LTL formula, which is the one having the W temporal operator in the paper.

Once you have the LTL formula, there is just one semantics, the "standard LTL semantics", that's it.

But clearly what I am saying has some bug, because the LTL formula I get when I ran:

syfco -f ltl test-strict.tlsf

does not have the strict shape.. (does not have the W)

In particular your text above:

• "There are two possibilities" ; and
• "Your assumption is that the ltl format is always interpreted under standard LTL semantics, which causes the problem with your understanding."

seems to suggest that an LTL formula can be read in different ways? I would indeed say that that once we have an LTL formula, that's it, we just use the "standard" LTL semantics. Isn't this correct?

The thing is that because the TLSF is NOT a formula, but a set of data structures, one can re-arrange the different parts in different ways to form an LTL formula. That is what I understood by "standard" vs "strict", different ways of building the LTL formula from the TLSF spec.

Now your turn... where am I wrong? (you are free to say "everywhere" ha!) ;-)