Constraints on workflow paths, part 4

Although I have not had much personal time lately, to finish the Pandamator code, I managed to move the workflow constraint checking forward, using LtlChecker as I promised in the relevant post. I’m not very happy with all the details — yet. Although I do call it ultimately from within C#, the work is done through F# code, so relying on parameter-less delegates, which in turn rely on mutable state, did not do me any good. I’m thinking of switching everything to use externally passed state, since using refs in F# is a sore sight indeed.

The reason I ended up using F# (except for the obvious reason that F# is more fun than C#) is that the code to generate workflow paths and interleave validation is very heavily recursive and intertwined. Meaning  that the 130 lines of F# would have been God knows what, had they been written in C#.

In what follows, I have elided details about the Scenario and the ScenarioStep because they don’t matter for this post. The central point is function pathsFromNode. Don’t worry about the partial match on the list, I make sure the list starts non-empty.

let rec pathsFromNode (f:ScenarioStep -> ConstraintResult -> ConstraintResult) ((step,res) :: path) (scenario:Scenario) =
    seq {
        let trans = (transitionsFromNode scenario step) |> Seq.toList
        if trans.Length = 0 then
            let res1 = f step res //run f one more time to simulate extension to infinite path
            yield (step,res1) :: path
        else
        for s in trans do
            if not (List.exists (fun (x,_) -> x = s) path) then
                let res1 = f s res
                if res1.status <> Failed then
                    yield! (pathsFromNode f ((s,res1) :: (step,res) :: path) scenario)
                else yield (s,res1) :: (step,res) :: path
    }

Note the line with the comment. It is necessary for the reason I explained in the last post (Büchi automata assuming infinite words). This function returns a sequence of paths, the generation of each path being able to end prematurely if the constraint validation fails along the way.

Since I am using LTL on single paths, I needed some way to extend this to all possible paths.  I do this the easy way, using ∀ and ∃.

let checkForallNever51 (scenario:Scenario) (step:ScenarioStep) =
    let step_ref = {new _step_ref with step=step}
    let dic = new Dictionary<string,System.Func> ()
    let p = Action(51)
    dic.Add("p",(fun () -> evalPredicate step_ref.step p))
    let con = create_constraint "G ! p" dic
    let i0 = init con
    if i0.status = Failed then
        (false, Some [step, i0])
    else
        let checker (step:ScenarioStep) (res:ConstraintResult) =
            step_ref.step  forall_ce (fun ((s,res) :: _) -> res.status <> Failed && res.status <> CannotTerminate)

let checkNever51After52 (scenario:Scenario) =
    let coisteps = scenario.steps |> List.filter (fun s -> s.actions |> List.exists (fun a -> a.id = 52))
    coisteps |> forall_ce2 (checkForallNeverSoi scenario)

Never mind forall_ce, it is like forall but returns a counterexample if it fails (annotated boolean, if you like). There is also an exists_ce with the same return type, but it always returns None since failing does not produce any counterexample. And the forall_ce2 variant accepts a predicate that returns an annotated boolean, as well. I know, the names suck but I couldn’t think of anything better.

As you can see, I am selecting the start nodes and run a ∀ on each of them. In this example, I am not starting from entry nodes of the workflow.

In the next example, I am starting from entry nodes, but (in a perverse twist) I also use the constraint validation with a ∃ for filtering the start nodes.

let checkEventually52 quantifier (scenario:Scenario) (step:ScenarioStep) =
    let step_ref = {new _step_ref with step=step}
    let dic = new Dictionary<string,System.Func<bool>> ()
    dic.Add("p",(fun () -> evalPredicate step_ref.step (Action(52))))
    dic.Add("q",(fun () -> evalPredicate step_ref.step (Action(51))))
    let con = create_constraint "F p & G ! q" dic
    let i0 = init con
    if i0.status = Failed then
        (false, Some [step, i0])
    else
        let checker (step:ScenarioStep) (res:ConstraintResult) =
            step_ref.step <- step
            next res
        let paths = pathsFromNode checker [(step,i0)] scenario
        paths |> quantifier (fun ((s,res) :: _) -> res.status <> Failed && res.status <> CannotTerminate)

let checkForallEventually52 (scenario:Scenario) (step:ScenarioStep) =
    checkEventuallyCoi forall_ce scenario step
    
let checkExistsEventually52 (scenario:Scenario) (step:ScenarioStep) =
    checkEventuallyCoi exists_ce scenario step

let checkEventually52After52Event (scenario:Scenario) =
    let coieventsteps = scenario.steps 
                        |> List.filter (fun s -> 
                                        ((stepHasInput s) && (fst (checkExistsEventually52 scenario s)))
                                        || (stepHasWebactionFor52 s))
    coieventsteps |> forall_ce2 (checkForallEventually52 scenario)

The quantifier is a parameter of checkEventually52. Granted, it is not the cleaner code imaginable. It is also not comparable to what CTL* (or plain CTL — I remind you that CTL allows quantifiers before any occurrence of a modal operator in an expression, not just at top level) would be able to express. However, it has proven that it is possible to express constraints a lot more declaratively than my ad-hoc Prolog program did. What remains now, is to use it to express useful constraints.

LtlChecker, part 2

When I described LtlChecker in the relevant post, I wrote I had made a mild effort to “make it more C# friendly” and I left it at that. However, it dawned on me that LtlChecker, combined with an exhaustive path generation on a workflow (the kind that F# sequences do effortlessly) can actually replace the ad-hoc approach I followed with my Prolog program (see the post on workflow constraints that started the whole affair). Stepping through the Büchi automaton for every transition of the workflow will prune the search space very effectively. It is not the same as having a CTL* checker, but serves the same purpose, since we are mostly covered if we get an implicit ∀ in front of all formulas (for which plain CTL is sufficient, to be frank).

So, in the end, it seems I’ll be able to join both threads (the one on workflow constraints and the one on temporal database constraints) using similar tools for both. Before doing that, though, which demands some more of my time than I currently have, I’ll present some caveats to you, and some actual C# code using LtlChecker (it was C#-friendly, after all).

First of all, you should know that Büchi automata are actually defined for infinite paths… which I thought did not matter while running it, but it actually does. I’ll revisit this point in the third test case below. For now, just keep in mind that a finite path supposedly repeats the final transition for ever and that’s how it’s made infinite to satisfy this precondition.

Second, I hinted at that in a casual comment in the LtlChecker code (ln.51), but did not spell it out in all detail: an accepting run of a Büchi automaton must pass through all acceptance conditions an infinite number of times. When you combine this with the above fact, the only way this can happen, is if the final transition (which will be mentally repeated infinite times) is actually marked with all of them. So, for finite paths (our case), any transition which it not accepting all acceptance conditions is as if it accepts none at all.

Let us look at some unit tests, now.

using System;
using System.Collections.Generic;

namespace CheckLtlUsageExample
{
    class Program
    {
        static void Main(string[] args)
        {
            Test1();
            Test2();
            Test3();
        }

        private static void Test1()
        {
            var obj = new[] { 0 };
            var dictionary = new Dictionary<string, Func<bool>> {{"p", () => obj[0] == 0}};
            var ltlConstraint = LtlChecker.create_constraint("G p", dictionary);
            var constraintResult = LtlChecker.init(ltlConstraint);
            var constraintResult2 = LtlChecker.next(constraintResult);
            var constraintResult3 = LtlChecker.next(constraintResult2);
            System.Diagnostics.Debug.Assert(constraintResult.status == LtlChecker.ConstraintStatus.CanTerminate);
            System.Diagnostics.Debug.Assert(constraintResult2.status == LtlChecker.ConstraintStatus.CanTerminate);
            System.Diagnostics.Debug.Assert(constraintResult3.status == LtlChecker.ConstraintStatus.CanTerminate);
        }
        private static void Test2()
        {
            var obj = new[] { 0 };
            var dictionary = new Dictionary<string, Func<bool>> {{"p", () => obj[0] == 1}};
            var ltlConstraint = LtlChecker.create_constraint("F p", dictionary);
            var constraintResult = LtlChecker.init(ltlConstraint);
            var constraintResult2 = LtlChecker.next(constraintResult);
            System.Diagnostics.Debug.Assert(constraintResult.status == LtlChecker.ConstraintStatus.CannotTerminate);
            System.Diagnostics.Debug.Assert(constraintResult2.status == LtlChecker.ConstraintStatus.CannotTerminate);
        }
        private static void Test3()
        {
            var obj = new[] { 0 };
            var dictionary = new Dictionary<string, Func<bool>> {{"p", () => obj[0] == 1}};
            var ltlConstraint = LtlChecker.create_constraint("F p", dictionary);
            var constraintResult = LtlChecker.init(ltlConstraint);
            obj[0] = 1;
            var constraintResult2 = LtlChecker.next(constraintResult);
            var constraintResult3 = LtlChecker.next(constraintResult2); //Extra step to simulate infinite path
            System.Diagnostics.Debug.Assert(constraintResult.status == LtlChecker.ConstraintStatus.CannotTerminate);
            System.Diagnostics.Debug.Assert(constraintResult2.status == LtlChecker.ConstraintStatus.CannotTerminate);
            System.Diagnostics.Debug.Assert(constraintResult3.status == LtlChecker.ConstraintStatus.CanTerminate);
        }
    }
}

Test cases one and two are straightforward.

Test case three exhibits a particular idiocyncrasy, which can be explained if one looks at the Büchi automaton itself.

It is not sufficient for SPOT to encounter “p”. This encounter must be followed by at least one other transition. This might be an artifact of the algorithms used to produce the automaton, but, since automata are supposed to apply to infinite paths, it is a right of the algorithm to do that. Which means that we must adapt to it… hence the extra “step” in test case three. There must always be an extra step in the end of a path, just in case.

I conclude with these words of caution, and I hope, by the next post, that either the path checking or the SQL implementation of running the automaton, will be completed so that I earn my bragging rights I’ve been working hard towards to.

LtlChecker: A spin-off of Pandamator

In the course of playing around with code to run the Büchi automata for the LTL constraint I’m adding to Pandamator, I realized that all that could be packaged into a nifty little feature for checking object evolution (or evolution of whole systems, for that matter). Enter LtlChecker, a library to help you apply the power of LTL to your imperative programs. Its only dependency is SPOT.fs from the Pandamator project, whose job is to execute SPOT and parse the automaton it produces. And SPOT itself, of course. I have took the easy way out regarding how SPOT is found: it must be in the path. Please note that cygwin1.dll must be on the path as well, for SPOT to be invoked.

SPOT.fs can be found in the SVN repository and, in any case, I have described it in the relevant post. I will focus on the new code, LtlChecker.fs. In an attempt to make it more C#-friendly, I have used Dictionary instead of Map.

Here’s a simple usage scenario, with which I will demonstrate how it works and I’ll present the implementation later.

type _test_struct = {
    mutable x: int
}

let _unit_test () =
    let obj = { new _test_struct with x=0 }
    let dic = new Dictionary<string,System.Func<bool>> ()
    dic.Add("p0",(fun () -> obj.x > 0))
    dic.Add("p1",(fun () -> obj.x > 0))
    let con = create_constraint "G(p0 -> G p1)" dic
    let i0 = init con
    obj.x <- 1
    let i1 = next i0
    obj.x <- 0
    let i2 = next i1
    obj.x <- 1
    let i2b = next i1
    (i0,i1,i2,i2b)

I have actually traced two diverging paths, for the constraint G(p0 -> G p1), where p0 and p1 both mean “property x of the test object is > 0”. The constraint can be translated as “once x becomes > 0, it never becomes zero again”.

Calling create_constraint creates an LtlConstraint, which is used to initialize the constraint checking. Calling init on it, evaluates propositions at the initial state and gives you back a ConstraintResult, which is what you’ll be examining throughout the constraint checking. The relevant property you should be looking at is status, an enumeration that tells you if the constraint has failed (Failed), if the system is at a state where it can be terminated with the constraint being fulfilled (CanTerminate), or if the system cannot be terminated now because the constraint awaits fulfillment (CannotTerminate).

Let’s look at it in practice. Here’s what i0 looks like.

{currentstates = [{state = 0;
                      accepting = true;}];
    status = CanTerminate;
    ltlconstraint =
     {automaton =
       {acccondnum = 1;
        states =
         [|{initial = true;
            transitions =
             [{endstate = 1;
               acccond = [0];
               guard = Bin (And,Prop "p1",Prop "p0");};
              {endstate = 0;
               acccond = [0];
               guard = Not (Prop "p0");}];};
           {initial = false;
            transitions = [{endstate = 1;
                            acccond = [0];
                            guard = Prop "p1";}];}|];};
      propositions =
       dict
         [("p0",
           System.Func`1[System.Boolean] {Method = Boolean Invoke();
                                          Target = LtlChecker+_unit_test@87;});
          ("p1",
           System.Func`1[System.Boolean]
             {Method = Boolean Invoke();
              Target = LtlChecker+_unit_test@88-1;})];};}

Status is CanTerminate, because x is still 0. In i1, status is still CanTerminate, and the current state is now state 1.

In i2, where x has gone to being 0 again, the status is Failed! That’s what one would expect.

In i2b, which is an alternative path from i1 but with x continuing to be bigger than 0, the status remains CanTerminate.

That’s is. A small facility to apply temporal logic in the evolution of mutable systems! In fact, you can apply it to any timeseries.

Nota Bene: I cannot guarantee that my interpretation of how running a Büchi automaton is done, is correct. It might happen that what works for the LTL expression above, might not work for some other expression. If I find problems (and manage to overcome them), I will update the code on SVN.

Here’s the code itself (it can also be found in the SVN repository, in project LtlChecker.

module LtlChecker

open System.Collections.Generic
open SPOT

type LtlConstraint = {
    automaton: BuchiAutomaton;
    propositions: Dictionary<string,System.Func<bool>>;
}

type ConstraintStatus = Failed | CanTerminate | CannotTerminate

type ConstraintState = {
    state: int;
    accepting: bool;
}

type ConstraintResult = {
    currentstates: ConstraintState list;
    status: ConstraintStatus;
    ltlconstraint: LtlConstraint;
}

let rec execute_logexp (propositions:Dictionary<string,System.Func<bool>>) (exp:LogicExpr) =
    match exp with
    | Const v -> v
    | Not e -> not (execute_logexp propositions e)
    | Bin (o, x, y) ->
        let lx = execute_logexp propositions x
        let ly = execute_logexp propositions y
        match o with
        | And -> lx && ly
        | Or -> lx || ly
        | Impl -> execute_logexp propositions (Bin(Or,Not(x),y))
        | Equiv -> execute_logexp propositions (Bin(Or,Bin(And,x,y),Bin(And,Not(x),Not(y)))) // (x and y) or (not x or not y)
        | Xor -> execute_logexp propositions (Bin(And,Bin(Or,x,y),Not(Bin(And,x,y)))) // (x or y) and not(x and y)
    | Prop p ->
        let rc = propositions.[p]
        rc.Invoke()

let create_constraint (ltl:string) (propositions:Dictionary<string,System.Func<bool>>) =
    let ba = ltl2ba ("'"+ltl+"'")
    { new LtlConstraint
        with automaton = ba
        and propositions = propositions
    }

let do_transitions (state:int) (con:LtlConstraint) =
    let states = con.automaton.states.[state].transitions
                        |> List.filter (fun t -> execute_logexp con.propositions t.guard)
                        |> List.map (fun t -> { new ConstraintState with state=t.endstate and accepting=t.acccond.Length>0 }) //Finite paths cannot work with more than one accepting condition
    states

let states_to_result (nextstates:ConstraintState list) (con:LtlConstraint) =
    let status =
        if nextstates.Length = 0 then
            Failed
        elif nextstates |> List.exists (fun s -> s.accepting) then
            CanTerminate
        else
            CannotTerminate

    { new ConstraintResult
        with currentstates=nextstates
        and ltlconstraint=con
        and status=status
    }

let init (con:LtlConstraint) =
    let initialstate = con.automaton.states |> Array.findIndex (fun st -> st.initial)
    let nextstates = do_transitions initialstate con
    states_to_result nextstates con

let next (res:ConstraintResult) =
    let nextstates = res.currentstates |> List.map (fun s -> do_transitions s.state res.ltlconstraint) |> List.fold (@) []
    states_to_result nextstates res.ltlconstraint

New Table Constraint Planned for Pandamator, part 2

As I promised in the previous relevant post, I am moving forward with the LTL constraint for Pandamator (as any of you who have been following the iteration on Flying Donut already know). Apart from some integration in the maintenance scripts, all that remains is actually running the Büchi automaton. Which, of course, is not an easy task to do in SQL… That’s why I’m going to stick to the positive side only, and give you an account of what I have done so far.

The actual syntax of the constraint is very close to what I wrote earlier (I used WITH instead of WHERE because it’s already used as a keyword for defining things).

alter table Production.Product 
add validtime constraint weightneverdec 
check 'G(p0 -> G p1)' 
with p0 = weight > 0, p1 = weight > 0

This is a simple constraint for testing, which means that, whenever Product.weight becomes bigger than zero, it never becomes zero again.

SPOT happily produces the following automaton for that expression.

2 1t
0 1
1 0 -1 & p1 p0
0 0 -1 ! p0
-1
1 0
1 0 -1 p1
-1

The automaton is parsed internally to the following value.

val it : BuchiAutomaton =
  {acccondnum = 1;
   states =
    [|{initial = true;
       transitions =
        [{endstate = 1;
          acccond = [0];
          guard = Bin (And,Prop "p1",Prop "p0");}; {endstate = 0;
                                                    acccond = [0];
                                                    guard = Not (Prop "p0");}];};
      {initial = false;
       transitions = [{endstate = 1;
                       acccond = [0];
                       guard = Prop "p1";}];}|];}

Almost the full definition for LBTT is followed by my (simple) parser, except I assume that states are named as consecutive numbers starting at zero, because SPOT does that.

The abstract syntax tree for the automaton is defined by the following types.

type LogicOp = And | Or | Impl | Xor | Equiv

type LogicExpr =
    | Prop of string
    | Const of bool
    | Not of LogicExpr
    | Bin of LogicOp * LogicExpr * LogicExpr

type BuchiAutomatonTransition = {
    endstate: int;
    acccond: int list;
    guard: LogicExpr;
}

type BuchiAutomatonState = {
    initial: bool
    transitions: BuchiAutomatonTransition list;
}

type BuchiAutomaton = {
    acccondnum: int;
    states: BuchiAutomatonState[];
}

A simple translation layer transforms the propositional logic of the guards, together with the definition of the propositions in the constraint, to SQL.

let rec logexp2stringlist (rcl:PropositionDefinition list) (exp:LogicExpr) =
    match exp with
    | Const true -> ["(1=1)"]
    | Const false -> ["(1=0)"]
    | Not e -> ["NOT";"("] @ (logexp2stringlist rcl e) @ [")"]
    | Bin (o, x, y) -> 
        let lx = logexp2stringlist rcl x
        let ly = logexp2stringlist rcl y
        match o with
        | And -> ["(";"("] @ lx @ [")";"and";"("] @ ly @ [")";")"]
        | Or -> ["(";"("] @ lx @ [")";"or";"("] @ ly @ [")";")"]
        | Impl -> logexp2stringlist rcl (Bin(Or,Not(x),y))
        | Equiv -> logexp2stringlist rcl (Bin(Or,Bin(And,x,y),Bin(And,Not(x),Not(y)))) // (x and y) or (not x or not y)
        | Xor -> logexp2stringlist rcl (Bin(And,Bin(Or,x,y),Not(Bin(And,x,y)))) // (x or y) and not(x and y)
    | Prop p -> 
        let rc = rcl |> List.find (fun rc -> rc.name = p)
        "(" :: rc.expression :: [")"]

During ALTER VALIDTIME execution, a view is created to abstract away the exact expressions used for the propositions (as boolean numbers 0/1, since SQL does not recognize logical expressions outside WHERE).

CREATE VIEW [Production].[Product_weightneverdec_GuardView] WITH SCHEMABINDING as
SELECT
 ProductID,
 ValidToDate,
 row_number() over (partition by ProductID order by ValidToDate) AS VersionOrdinal,
 case when ( ( ( weight > 0 ) ) and ( ( weight > 0 ) ) ) then 1 else 0 end AS g0_0,
 case when NOT ( ( weight > 0 ) ) then 1 else 0 end AS g0_1,
 case when ( weight > 0 ) then 1 else 0 end AS g1_0
FROM [Production].[Product]

That’s it. I wish I had done more, but I believe I made good use of my scant free time to do as much as possible. Expressed like that, the view can be used to perform (non-deterministic, i.e. parallel…) runs of the automaton on the actual object histories. Stay tuned, I hope my next post on the subject will be a triumphant conclusion to creating the constraint.

New table constraint planned for Pandamator (Constraints on workflow paths, part 3)

Building upon the thoughts in part 1 and part 2 of this series of posts, I’m planning a new table constraint for Pandamator.

First of all, I have created Pandamator as a public project in the Flying Donut tool. So you’ll be able to keep tags on me while I’m moving Pandamator forward. Once you’re at it, you can register for free, and use it for your own projects. Don’t worry if you are not an expert Donut Flyer, a sample project will be created for you to play with upon your registration. I have great hopes for this tool and I have actually invested for its development. So I’m putting my money where my mouth is, by using it for Pandamator!

You’ll find an iteration (SCRUM terminology) for the new table constraint, there, so I’m not going to explain breakdown into items and tasks. I’m going to give you the outline of how I’m planning it to work. It’s the first big addition that diverges from ATSQL. Here’s what I’m thinking it should look like.

ALTER TABLE T ADD VALIDTIME CONSTRAINT C CHECK('[] p1 -> <> p2')
WHERE p1 = AMOUNT > 100, p2 = POSITION > 2

It’s a variation of the CHECK constraint, where the constraint is not a logical expression, but a string. This is done so that the constraint itself will be whatever SPOT accepts (LTL and PSL), without interfering with SQL grammar. The connection to SQL grammar will be in the WHERE clause that follows this novel CHECK constraint, which will provide the meaning of the propositions, inside LTL/PSL, as SQL expressions on the object in question. I settled on that as a solution to ensure separation of concerns and a smooth transition between the two domains. SPOT will do its job, and create the Büchi automaton, and Pandamator will generate proper SQL for the propositional logic formulas within, by plugging in the propositions defined in the constraint. Before that, I toyed with grandiose ideas of extending the SQL grammar to add LTL/PSL, but the solution I’m proposing here seems a lot cleaner, in the end.

I’ll post an update when this progresses a bit, and you can keep track of it yourselves at the relevant iteration.

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…