X	LTL Operator "Next"
U	LTL Operator "Until"
R	LTL Operator "Release"
Not	logical "not"
:/\:	logical "and"
:\/:	logical "or"
TT	logical "true"
FF	logical "false"
-->	logical implication

Types and Data structures

The main type is LTL a which represents a valid LTL formula. The leaves of the formula are the

StateProps Prop a . (Also: Props a as a set.)
TemplateF a b is the type for our template mechanism. We provide a template tree for efficient storing of (partial-) templates. But you are free to implement your own template handler using the Template State.
TTBranch a b provides our built-in template tree.
TStateF a b is the type for template state.
TemplateFs a b is used for storing all templates and the corresponding stateProps (which were added since the template has been installed).
CheckerState a: State of the verifier.
CheckerParam: Global parameters of the verifier.
All other types are either self explaining or obsolete.

Overview: Functions provided by our library

You can either install a LTL-formula directly ( installFormula <name> <formula>) or by using the template mechanism. By default the the templates are stored in a tree ( installTemplateTree <name> <template>). Disadvantage of our tree is that we generate every permutation of the relevant stateProps (i.e. the Properties which were set since the template has been installed). Unfortunately this is necessary as we don't have any further information about the properties; i.e. if they depend on each other. But you have, so it may be more efficient to implement your own permutation algorithm and template tree (if you like) using the Template State.

setProp <properties>	Sets a list of properties (stateProps).
releaseProp <properties>	Releases a list of properties (stateProps).
step	Forces the verifier to evaluate all registered LTL formulae. Note: Implicitly done by MVar functions from ConcLTL.hs.
verif	Forces the verifier to evaluate all registered LTL formulae, but doesn't make any changes to the formula dictionary (the registered formulae).
notify	Stops all threads instead of verifier and forces the execution of every command in the command queue.
showProps	Displays all current stateProps.
showChecks	Displays all current LTL formulae.
showTemplates	Displays all current templates with corresponding template tree if present.
showNumChecks	Displays the number of registered formulae.
showTrace	Displays the complete trace of stateProps.
showTTreeAnalysis	Displays rough information about the template tree.
showUsedProps	Displays the currently used props of installed formulae (i.e. intersection of stateProps and all properties of every registered formula).
getTrace	Returns the complete trace of stateProps.
noStateF	Dummy function for state mechanism if built-in template trees are used.
noState	Dummy function for state mechanism if built-in template trees are used.

Some other internal functions may be useful for you if you use the Template State.

genAndCheck <template> <stateProps>	Calls generate2 with stateProps as list and the cardinality of the given template as length of permutations. Calls check with results of generate2 with the resulting permutations as parameter
gen <template> <stateProps>	Like genAndCheck but without calling check. Returns the result of generate2
check <permutations> <template>	Applys all permutations to the given template function and returns list of either new templates, new formulae or nothing. Nothing is returned if none of the guards (template function) matched the given permutations, a new formula if all free variables are instantiated and a new template if there is a partial template and the program was able to instantiate a part of the template.
generate2 <list to permutate> <length of permutations>	Generates all permutations with a specified length of an arbitrary list.
generate <list to permutate> <length of permutations>	Like before, but uses other algorithm.

Simple LTL formulae

Simple LTL formulae are installed installFormula <name> <formula>. Once installed, the verifier tries to (in)validate the formula with each step (function checkStepList in LTL.hs). It takes the formula and the current stateProps and simplifies the formula as much as possible (function checkStep in LTL.hs). If the formula is reduced to true or false the verifier halts and prompts a message. Otherwise the reduced formula is optionally checked if it contains a circle and stored in the second component of the CheckerState.

Example: (Philosophers.hs)
Dining philosophers (wlg five philosophers)
We want to prevent that every philosopher takes his left stick (StateProp (StringProp c k) means that k has taken his left stick (c k)).


   notDeadPhil :: LTL String
notDeadPhil = g (Not (foldr1 (\phi psi -> (phi :/\: psi))
		             (map (StateProp . StringProp) ['c':show i | i <- [1..5]])))

The presented formula assures that all left sticks are never (globally not) taken the same time. Every time a thread (philosopher) k takes its left stick it will set the appropriate StringProp c k afterwards. If it is able to grab also the second stick, the Properties is released again as this thread can't cause a deadlock (both sticks are put back after eating). On the other hand all other StringProps may be set too. In that case the verifier will print a warning.

Using Template Trees to generate LTL formulae

In some Applications defining a simple LTL formula is not adequate. In that case you may want to use a template which generates several new formulae for you. A template is a Haskell function which takes a list of stateProps as argument, i.e. all permutations of a predefined length of all stateProps set since the template is alive.
Type of the template:


   newtype TemplateF a b = TF (Int, ([Prop a] -> Maybe (Either (TemplateF a b) (LTL a))), TStateF a b, b)

where the parameters are (fltr): Cardinality, template function, state transition function, initial state). The cardinality indicates the length of permutations generated by the genAndCheck or gen function. The template function receives a list of permutations. State transition function and initial state are just for templates with generic state. Use noStateF and noState as dummy functions.
Most of the work is done in the template function.
Designing the template function: Take as many properties as you need (make sure the cardinality is greater or equal) and define some guards, e.g. if Prop1 equals Prop2 then install new formula. If your formula is partial instantiable it is also possible to generate a new template (see paper for further details).
Install the template tree with the command installTemplateTree <name> <template>. Our template tree contains generated LTL formulae as leaves and partial templates as nodes (more precisely: The properties which were used to instantiate the template at that node).

Example (Lock-reversal): (ManyLockReversal.lhs)
As mentioned in our paper, one application of our library is to prevent deadlocking of concurrent processes. Assume we have a process which takes two locks in a specific order (say A B) and another process which takes the same locks in reverse order. In that case we want the debugger to display a warning.
The example program ManyLockReversal.lhs takes three arguments: The number of threads, the number of locks and either partial or non partial (i.e.: if the program should use the improvements of partial instantiation or not (see paper or source code)).

Detailed explanation of partial template


   This template has cardinality 2, which means that it takes the first two arguments of the property-list (line marked with *-*). 
All permutations of stateProps in order to instantiate this template have also length 2. 
The last two arguments are not used (reserved for the state template mechanism).

> lockReversal :: TemplateF String b 
> lockReversal = TF (2 , lockF, noStateF, noState) 

lockF gets a list of properties and returns either a new template or a fully instantiated new LTL formula      
lockF takes the two first properties (IntProps in this case) and discards the rest of the list (_). 
i1 and i2 are the thread id's and x1 and y1 are variables representing two locks. 



> lockF :: (Eq a) => ([Prop a] -> Maybe (Either (TemplateF a b) (LTL a)))
> lockF (p1@(IntProp i1 x1):p2@(IntProp i2 y1):_) -- *-*

If the thread id's are equal and the locks are different we can generate a new template with the first two arguments fixed.

>   | i1 == i2 && x1 /= y1 = (Just . Left) $ 
>     TF (2, (\x -> lockF2 (p1:p2:x)), noStateF, noState)



> lockF2 :: (Eq a) => ([Prop a] -> Maybe (Either (TemplateF a b) (LTL a)))
> lockF2 (p1@(IntProp i1 x1):p2@(IntProp i2 y1):
>         p3@(IntProp j1 y2):p4@(IntProp j2 x2):_)

More guards: If valid we can instantiate the whole formula (line marked with *-*). It will be installed afterwards.

>   | j1 == j2 && x2 /= y2 && y1 == y2 && x1 == x2 
>     = (Just . Right) $ (lockF' p1 p2) --> (g (Not (lockF' p3 p4))) -- *-*



> lockF' :: (Eq a) => Prop a -> Prop a -> LTL a 
> lockF' p1 p2 = (((StateProp p1) :/\: (Not (StateProp p2))) 
>                :/\: ((StateProp p1) `U` (StateProp p2)))

Detailed explanation of non-partial template


   This template has cardinality 4, which means that there will be s^4 many permutations generated (where s is the number of 
stateProps)

> lockReversal2 :: TemplateF String b
> lockReversal2 = TF (4, lockF3, noStateF, noState)

> lockF3 :: (Eq a) => ([Prop a] -> Maybe (Either (TemplateF a b) (LTL a)))
> lockF3 (p1@(IntProp i1 x1):p2@(IntProp i2 y1):
>         p3@(IntProp j1 y2):p4@(IntProp j2 x2):_) 

Guards: If valid we can instantiate the whole formula (line with *-*). It will be installed afterwards.

>   | i1 == i2 && x1 /= y1 && j1 == j2 && x2 /= y2 && y1 == y2 && x1 == x2 
>     = (Just . Right) $ (lockF' p1 p2) --> (g (Not (lockF' p3 p4))) -- *-*



> lockF' :: (Eq a) => Prop a -> Prop a -> LTL a 
> lockF' p1 p2 = (((StateProp p1) :/\: (Not (StateProp p2))) 
>                  :/\: ((StateProp p1) `U` (StateProp p2)))

Note: Make sure the "CheckTrace" flag is set.

Using templates with generic state

As mentioned before you can either use our built-in template tree or the template state. To do that install the formula with the installTemplate <name> <template>.
The template itself has the type


   newtype TemplateF a b = TF (Int, ([Prop a] -> Maybe (Either (TemplateF a b) (LTL a))), TStateF a b, b)

where the parameters are (fltr): Cardinality, template function, state transition function, initial state. The cardinality indicates the length of permutations generated by the genAndCheck or gen function and is unnecessary if you decide to generate the permutations yourself. Note: Make sure you generate permutation with the minimum length l, where l is number of list members the template function takes. The template function receives a list of permutations and throws either a new (partial) template or a complete LTL formula which can be installed.
The last two arguments contain the interesting part: The initial state is just a polymorphic type can represent everything you wish, in particular something to generate the permutations. The state transition function takes one state, the template itself and the current stateProps. You have to take these arguments, generate whatever you want, apply some permutations to the template function, handle the results and install possible new templates or LTL formulae.

Example: (StateEx.lhs)
The example traces the stateProps, generates all permutations of the trace and counts the number of installed formulae.

Templates with generic state (cut-out of example)


   In that example the state is a tuple of stateProps and a counter. The initial state is (emptySet,0) 
(not set here, see source). The stateProps will be used to generate the permutations for the template function.

> type MyState = (Props String,Int)


 
> stateF :: TStateF String MyState
> stateF = TSF (stateF')

stateF' is the state transition function. It receives the template itself (especially the template function), 
the old state, the current stateProps of the verifier (i.e. which properties are set at runtime) and returns 
a new state.



> stateF' :: (TemplateF String MyState -> MyState -> Props String -> IO MyState)
> stateF' this (oldProps,count) props = do
>   putStrLn ("already " ++ (show count) ++ " formulae")

The new properties will be the union of the old state and the current stateProps.

>   let newProps = oldProps `union` props

genAndCheck is a built-in function you may use. It generates all permutations of its second parameter and 
checks the given template against these permutations. Result is a list of either a new template, a new LTL formula
or Nothing (i.e. none of the guards of the template function matched). Note: genAndCheck returns a tuple, but
the second component is not needed here and will be discarded.

>   perms <- (genAndCheck this (setToList newProps))
>   numNew <- mapM myCheck perms

myCheck returns a list of 0's and 1's (as many 1's as there are new formulae). newC contains the new value of installed formulae.

>   let newC = (foldr (+) count numNew)
>   putStrLn ("now " ++ (show newC) ++ " formulae")

The new state is the tuple of the new properties and the new counter value.

>   return (newProps,newC)



myCheck receives that tuple, installs a new formula and returns 1. Due to the used template in that example 
(non partial) there won't be any new template.

> myCheck :: ((Either (TemplateF String MyState) 
>               (Maybe (LTL String))),[Prop String]) -> IO Int
> myCheck (result,_perms) = 
>   case result of 
>     Right (Just phi) -> do
>                           id <- getFormulaId
>                           installFormula ("newPhi" ++ (show id)) phi 
>                           return 1
>     Right (Nothing) -> return 0
>     Left (temp) -> putStrLn "you will never reach this case" >> return 0

Compile Hints

Compile all examples separate with <ghc> --make <filename.hs> -o <output>

Appendix A : Types of properties

Some useful state properties for the verifier are predefined. Most properties contain a polymorphic type variable, particularly the MyProp property you may easily use for your own property type. You may also extend the data structure itself. The stateProps are the "leaves" of LTL formulae.

StringProp String	Property for Strings.
IntProp Int a	Property for an Ints and an arbitrary type.
ThreadProp ThreadId a	Property for a Thread ID and an arbitrary type.
TProp (Int,Int) a	Property for a tuple of Ints and an arbitrary type.
MyProp a	Property for an arbitrary type.

Appendix B : Checker Parameters

The verifier has several optional parameters. Apply these in file LTL.hs at function checkThreadMVar.

FindCycle	If set, the function checkStepList searches for cycles in reduced LTL formula. Condition: the formulae have to be identical and the state must be the initial state (i.e. intersection empty).
UsedParams	Optimization: For every installed LTL Formula is a usedProps flag stored. If set, the function checkStepList is applied only, if flag is true. (Flag is true if current stateProps intersect non-empty with properties in the formula).
CheckTrace	If set, every new template is checked against the whole stateProp trace. Useful e.g. in a case where the program would deadlock exact at the same time as the LTL condition is violated, but it may be violated before the template has been installed e.g. in the Example "lock reversal".
CutPhiTrace	When a LTL formula is violated the verifier displays the trace of stateProps which lead to the falsification. You optionally can cut this trace of using that parameter and by setting the lengthPhiTrace constant in LTL.hs.
CutGlobalTrace	If set the global trace (used by template mechanism, see parameter CheckTrace) is cut to the length given by lengthGlobalTrace in LTL.hs.
Stuttering	If set, the global trace doesn't store equal consecutive stateProps.
Verbose	If set, the verifier displays more debug information.

Appendix C : Checker State

The checker state stores the installed LTL formulae and some information about them. It's a 4-tuple with the following elements: original installed formula, current formula (reduced by checkStep), trace since LTL has been installed (may be cut of, see Checker Parameters) and a flag if the current stateProps are used in this formula (see Checker Parameters).
Note: The trace is cleared if a cycle occurred (see Checker Parameters).

René Theisen, Volker Stolz

Volker Stolz

Disclaimer

Last modified: 2004-04-30 07:10 UTC