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
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@lrde.epita.fr To unsubscribe send an email to spot-leave@lrde.epita.fr
-
Mark Santolucito -
philipp