differences between syfco's lily examples, and the original examples from Lily

[adl]

Is anyone able to point the original source of examples/lily/lilydemo24.tlsf?

Lily 1.0.2, as distributed on its home page, only comes with 23 examples (and its paper only mentions 20). I'm curious where this one is coming from. Looking for other examples with similar subformulas, this could be a subclause of examples/acaciaplus/genbuf2.tlsf.

[adl]

Comparing Syfco's examples in lily/ with the original examples of the Lily distribution, I'm finding some divergences.

For instance Lily 1.0.2's demo-v15.ltl file contains:

G(r1=1 -> F(a1=1));
G(r2=1 -> F(a2=1));
G(!(a1=1 * a2=1));
(a1=0 U r1=1) + G(a1=0);
(a2=0 U r2=1) + G(a2=0);

which is realizable. But Syfco's lilydemo15.tslf has

  INVARIANTS {
    r1 -> F a1;
    r2 -> F a2;
    !(a1 && a2);
  }

  GUARANTEES {
    a1 W r1;
    a2 W r2;
  }

which isn't realizable. (a1 and a2 should be negated in the guarantees.)

demo-v16.ltl differs from lilydemo16.tlsf in exactly the same way (missing negations).

[adl]

Since I'm complaining about example files, I should probably add some context.

I'm trying to equip Spot with the necessary machinery to build random conjunctions of LTL specification formulas, as done in Section 3.2 of this paper. Since that paper used Lily's formulas as base formulas to be combined, I wanted to try with that same set as input, and decided it was easier to ask syfco to rewrite its lilydemo*.tslf files in my syntax, rather than having to deal with Lily's original syntax. Then I noticed the extra example, as well as the cases that I could not solve (with Mealy semantics) even when LiLy's README states that they are realizable (with Moore semantics).

I'd suggest to update these examples to match the original ones, or to rename them. The current discrepancies might cause people to compare results that are not comparable.

[gaperez64]

do you know if the lilydemo benchmarks in the official benchmark repo are also different than the ones from the original lily repo?

[adl]

Yes, there is the same problem over there (they have lilydemo24, and they are missing some negation in lilydemo{15,16}).

The only difference between these two repositories is that the lilydemo files in Syfco say SEMANTICS: Moore while those in Benchmark use SEMANTICS: Mealy instead. Lily uses Moore semantics, so that probably make Benchmarks further away from the original source.

[adl]

To follow up on the fact that Lily 1.0.2 has only 23 demos, but syfco & syntcomp have 24. I came across https://github.com/gaperez64/acacia_ltl2aig/tree/master/examples/demo-lily which has 25 demos... Demo 24 matches. I'd love to rewind history, but Acacia+ seem to have disappeared from the web.

[gaperez64]

Ah! That's a great lead! I found in the thesis of Aaron Bohy a mention of the lily-demo examples having been modified for the purpose of benchmarking Acacia+. The code and examples in the repo you mentioned were handed to me by Aaron himself after he finished his PhD so we should indeed rename the examples to acacia_plus_lily or something like that.

On Fri, 20 Sept 2024 at 17:43, Alexandre Duret-Lutz < @.***> wrote:

To follow up on the fact that Lily 1.0.2 has only 23 demos, but syfco & syntcomp have 24. I came across https://github.com/gaperez64/acacia_ltl2aig/tree/master/examples/demo-lily which has 25 demos... Demo 24 matches. I'd love to rewind history, but Acacia+ seem to have disappeared from the web.

— Reply to this email directly, view it on GitHub https://github.com/reactive-systems/syfco/issues/55#issuecomment-2364018034, or unsubscribe https://github.com/notifications/unsubscribe-auth/AAUJJ2LKHADR7DTFYRNYWMTZXQ7ALAVCNFSM6AAAAABNDW6TP6VHI2DSMVQWIX3LMV43OSLTON2WKQ3PNVWWK3TUHMZDGNRUGAYTQMBTGQ . You are receiving this because you commented.Message ID: @.***>