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.

Fp-ba-graph

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.

Advertisements

One thought on “LtlChecker, part 2

  1. Pingback: Constraints on workflow paths, part 4 | dsouflis

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s