Continuing the effort to express constraints on workflow paths from the previous post, here is some practical advice for those who wish to undertake something similar, or simply retrace the same road.
First of all, I settled on SPOT. This was done for the following reasons: its on-line LTL-to-TGBA translator, as they call it, makes it easy to experiment; it can help you rephrase your LTL using automatic simplifications; it can output many different visual formats; its standalone executable can output standard LBTT; and, what I found quite helpful, it actually understands PSL in addition to LTL. PSL is a language “for specifying properties or assertions about hardware designs”. PSL supports SEREs (Sequential Extended Regular Expressions), which are formed like regular expressions, and can be combined with LTL expressions using special binding operators. Even though the whole expression can ultimately be expressed fully in plain LTL (and SPOT can formulate it that way for you), I found it easier to start with a SERE.
Which brings me to the formulation I arrived at for the property that troubled me in the end of the previous post:
G(soi -> X(!input U (input & Fcoi))) (which SPOT can also output in fancy Unicode:
□(○(¬input U (input∧◇coi))∨¬soi)). Its Büchi automaton is the following:
And here it is on the Web. Looks daunting, but you get used to it after a while. Let me show you how to produce it from the command line (Cygwin shell, in my case).
ltl2tgba -f 'G(soi -> X(!input U (input & Fcoi)))' --lbtt --ba
The LBTT output is the following.
4 2t 0 1 0 0 1 -1 ! soi 1 0 1 -1 soi -1 1 0 0 0 1 -1 & & ! soi input coi 1 1 -1 ! input 1 0 1 -1 & & soi input coi 2 0 -1 & & soi input ! coi 3 0 -1 & & ! soi input ! coi -1 2 0 0 0 1 -1 & & ! soi input coi 1 1 -1 & ! input coi 1 0 1 -1 & & soi input coi 2 -1 & ! input ! coi 2 0 -1 & & soi input ! coi 3 0 -1 & & ! soi input ! coi -1 3 0 0 0 1 -1 & ! soi coi 1 0 1 -1 & soi coi 2 0 -1 & soi ! coi 3 0 -1 & ! soi ! coi -1
To link the two, I have prepared an image where I link the first few transitions in the LBTT output to those on the automaton image.
You can take it from there…
The point of this exercise is the following: If you express your property in LTL and you’re prepared to jump through a few hoops, it is possible to invoke SPOT and read back a Büchi automaton for it, which you can use either to check your model, or as a run-time constraint checker. Now, there are ways to interface to SPOT so that you can provide your state space, as they call it, and SPOT will verify if the intersection of it with the automaton is empty or not. I have not explored it further. But using the resulting automaton as a generator for constraint-checking run-time infrastructure seems like what I wanted to do in Pandamator ever since I read about LTL.
I’m happy to close this post with a positive feeling! It’s not the end of the story, I promise you…