Constraints on workflow paths, part 2

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…

Constraints on workflow paths

I have mixed feelings about the current post. For the specific problem at hand, I had intended to develop a series of solutions, the one represented here being just the first one, soon to be replaced by a better one. However, for reasons I am going to go into later, I settled for this one, for the time being.

The domain of discourse is: workflow specifications, and how to verify them. Wide and under-specified enough to make for an interesting problem. My first thought for a quick-and-dirty solution, which would give some immediate results until the more elaborate ones brewed, was to develop a program to evaluate some pertinent constraints on possible paths through the workflow, and my choice for the language to use was Prolog. The reason is the painless facilities it has for state-space exploration: backtracking, incremental elaboration of data and pattern-matching through unification and conciseness. Plus, back in the ol’ days, I considered myself a decent Prolog programmer. Now, it could be debated whether tag “Esoteric” is really suitable for Prolog . After all, it has been around for more than forty years, and most universities teach it. However, it remains impenetrable for the uninitiated, and I don’t think many people actually learn it, even if they are taught about it.

For reasons unknown I had to start with Visual Prolog. Probably because I had avoided Turbo Prolog when it came out and I never had more than a casual glance at Mercury, Oz and other multi-paradigm languages.  That phase lasted the better part of two days, then I got fed up with the nagging message at startup and I went back to the less flashy SWI Prolog.To make a long story short, what I did was the following. My program loops through all of our workflows, reads them as Prolog facts and then runs the actual verification code on each one. The focus of this post is the actual verification code running on the graphs which encode the workflows.

Each verification rule looks for counter-examples of the property it encodes, which are paths through the graph. It consists of the following components: a selector of initial nodes, a filter that limits the edges taken from each node, and a selector of final nodes. Other than limiting the search space with the aid for those components, exploration is exhaustive, since we’re looking for counterexamples.

For example, the following clauses of the filter predicate for a particular rule, encode some workflow conditions on having or not having passed through a prior workflow step (and the lack of syntax highlighting for Prolog from WordPress certainly justifies the “Esoteric” tag).

allowed_arc(N,V) :-
	stepcond(N,through(I)),
	member(I,V),
	!.
allowed_arc(N,V) :-
	stepcond(N,not_through(I)),
	member(I,V),
	!, fail.

As you can see, the filtering predicate takes as parameters the node to go to, and the sequence of previously visited nodes. The filtering predicated is called by predicate possible_path, which computes the path.

possible_next(V, Pr, X, Y) :-
	stepact(X,goto(Y)),
	apply(Pr,[Y,V]).
possible_next(V, Pr, X, Y) :-
	stepcond(Y,input(_)),
	X \= Y,
	apply(Pr,[Y,V]).

possible_path(V,_,X,X,P) :-
	reverse(V,P).
possible_path(V, Pr, X, Z, P) :-
	possible_next(V,Pr,X,Y),
	possible_path([Y|V],Pr,Y,Z,P).

Evaluating the rule is done with the help of findall.

findall(
	P,
	(stepact(F,soi),
		possible_path([F],allowed_arc,F,Z,P),
		length(P,L),
		L > 1,
		stepact(Z,soi)),
	X4)

It needs a second look, so let me break it up.

stepact(F,soi) Start from every action matching the particular fact pattern.

possible_path([F],allowed_arc,F,Z,P) Enumerate all possible paths using the particular filter.

length(P,L), L > 1, stepact(Z,soi) Stop for all paths of length > 1 whose final node matches the particular fact pattern.

A brute-force solution, but managed to sniff out several potential problems in the workflows and has room to grow with new rules. Why did I say that its only purpose was to pave the way for more elaborate solutions?

My hope was to use formal verification methods, and I had every reason to be hopeful because I had multiple candidates to try.

The first one was UPPAAL, a tool which allows one to specify timed automata, simulate them and verify invariants expressed in CTL. Sounds cool, doesn’t it?

The problem is, encoding your system in this way is not an easy task, and probably not something that could be done by translating a workflow specification automatically. And people who used it independently had trouble adapting the tool to their problem and ended up actually playing to the strengths of the tool. It’s not out the question, but it needs a lot of time and dedication, and it is not a short-term study.

My other hope was to express the path constraints using LTL, instead of the unstructured way I was using. Which necessitated a lot of research to find how LTL can be verified and what tools there are to aid one in this endeavor. It turns out there are, and some of them have been also put online for people to test! Try out LTL2BA and SPOT. And, if you persevere through various tortures imposed on you by the intricacies of cross-platform C/C++ builds, you can actually find yourself with real singing and dancing LTL2BA and SPOT executables that you can invoke. Best of all, they can both be made to output (semi-?) standard LBT format. To give you an idea, the formula G p3 | (F p0 & F p1) results in the following Büchi automaton (yes, that’s what it’s called) which can be used to verify it at run-time.

This was something I’ve been considering for Pandamator, as well, to express constraints for whole object lifetimes. As I found out, it was not a novel idea, but maybe I’d have the honor of implementing it first in an accessible way. It would need some elaborate machinery: abstract away all logic that is not LTL (formulas to translate have simple propositional variables), invoke an external program, read back the automaton and fill back in the actual logic conditions. That would replace my hodge-podge filters and selectors with something having real logical backing. The problem is, trying to write the darned LTL constraints proved to be not evident!

For example, how would the following be written? After action p0, action p2 cannot appear unless condition p1 appears between them. My guess would be p0 -> X G ((!p1 & !p2) U (p1 U p2)). However, the automaton does not seem to be suitable.

This is my current situation… Maybe an intermediate solution would be to formulate an automaton directly, and use it as the specification of the constraint.

I won’t pretend I know the answer. I’m in the dark, but I’m determined to see this through. And, in the meantime, my lowly Prolog program can actually chug along and produce useful results…