15 Feb
2022
15 Feb
'22
10:36 p.m.
Hi Mark,
thanks for the compliments and we are happy to see the "synthesis" part
of spot
being used.
To your question:
I assume x and y are outputs /controllable APs and p1 is the input?
Should I understand the "[!0&!1&!2 |
0&1&!2] 1" to mean that when !2
is true, the system is free to choose from !0&!1 or 0&1?
In short: Yes.
Longer answer: the main assumption on the input is violated
and therefore the controller is free to do as he pleases.
ltlsynt does a lot of different things "under the hood".
One of them is to reduce the size of the mealy machine implementing
the specification.
So the edge could be labelled simply with [!2] and all choices
for the controller are ok, however by restricting it to [!0&!1&!2 |
0&1&!2]
we are able to generate a smaller machine.
Please find attached a jupyter notebook detailing the different
synthesis steps
for your example making it easier to follow.
To your second question:
You could in theory restrain your mealy machine to the part where the
assumption holds.
However I don't really see the advantage of it.
Infact, in this example, since there is no link between p1 and (x,y),
you could simply
omit the assumption part all together.
Please let me know if you need some additional information.
Best regards
Philipp
Le 2022-02-14 17:56, Mark Santolucito a écrit :
> Hi there,
>
> Thanks so much for the great tool! I am having trouble understanding
> the disjunction on state transitions. For example, I have the
> following small spec:
>
> ASSUME {
> G (p1);
> }
>
> GUARANTEE {
> G ((x) && (! (y)) ||
> ((y) && (! (x))));
> G (F x);
> G (F y);
> }
>
> From this, ltlsynt gives me:
>
> AP: 3 "x" "y" "p1"
> acc-name: all
> Acceptance: 0 t
> properties: trans-labels explicit-labels state-acc deterministic
> --BODY--
> State: 0
> [!0&!1&!2 | 0&1&!2] 1
> [!0&1&2] 1
> State: 1
> [!0&!1&!2 | 0&1&!2] 1
> [0&!1&2] 0
> --END--
>
Should I understand the "[!0&!1&!2 |
0&1&!2] 1" to mean that when !2
is true, the system is free to choose from !0&!1 or 0&1?
>
> On a related note, due to the ASSUME in the spec, !2 should never be
> true anyway. Is there a way to filter this out of the model? For
> context, I am really looking to get a Mealy Machine out of ltlsynt
> which I can then convert into program code that would run in an
> infinite loop. Maybe I am just going about this the wrong way?
>
> Mark
> _______________________________________________
> Spot mailing list -- spot(a)lrde.epita.fr
> To unsubscribe send an email to spot-leave(a)lrde.epita.fr