On Wed, Nov 11, 2020 at 2:38 PM Philip Schwartz <pschwartz090(a)gmail.com> wrote:
I read my previous email and I thought maybe I was not
clear enough:
My problem is transferring the "until" operator to an action recognized by spot
(such as ! ).
That's making it even more confusing.
Spot only supports automa labelled by Boolean formulas over atomic propositions.
If you really expect to label an edge by an LTL formula, can you
describe the semantic of such an edge ?
--
Alexandre Duret-Lutz