Maintainer	Guilherme G. Azzi <ggazzi@inf.ufrgs.br>
Stability	provisional
Safe Haskell	Safe
Language	Haskell2010

Logic.Ctl

Contents

CTL Expressions
Model checking

Description

Synopsis

CTL Expressions

data Expr Source #

CTL expressions

Constructors

Literal Bool
Atom String
Not Expr
And Expr Expr
Or Expr Expr
Implies Expr Expr
Equiv Expr Expr
Temporal (PathQuantified Expr)

Instances

Eq Expr Source #
Methods (==) :: Expr -> Expr -> Bool # (/=) :: Expr -> Expr -> Bool #
Read Expr Source #
Methods readsPrec :: Int -> ReadS Expr # readList :: ReadS [Expr] # readPrec :: ReadPrec Expr # readListPrec :: ReadPrec [Expr] #
Show Expr Source #
Methods showsPrec :: Int -> Expr -> ShowS # show :: Expr -> String # showList :: [Expr] -> ShowS #
Pretty Expr Source #
Methods pretty :: Expr -> Doc prettyList :: [Expr] -> Doc

data PathQuantified e Source #

Path-quantified CTL expressions

Constructors

A (StateQuantified e)
E (StateQuantified e)

Instances

Eq e => Eq (PathQuantified e) Source #
Methods (==) :: PathQuantified e -> PathQuantified e -> Bool # (/=) :: PathQuantified e -> PathQuantified e -> Bool #
Read e => Read (PathQuantified e) Source #
Methods readsPrec :: Int -> ReadS (PathQuantified e) # readList :: ReadS [PathQuantified e] # readPrec :: ReadPrec (PathQuantified e) # readListPrec :: ReadPrec [PathQuantified e] #
Show e => Show (PathQuantified e) Source #
Methods showsPrec :: Int -> PathQuantified e -> ShowS # show :: PathQuantified e -> String # showList :: [PathQuantified e] -> ShowS #

data StateQuantified e Source #

State-quantified CTL expressions

Constructors

X e
G e
F e
U e e

Instances

Eq e => Eq (StateQuantified e) Source #
Methods (==) :: StateQuantified e -> StateQuantified e -> Bool # (/=) :: StateQuantified e -> StateQuantified e -> Bool #
Read e => Read (StateQuantified e) Source #
Methods readsPrec :: Int -> ReadS (StateQuantified e) # readList :: ReadS [StateQuantified e] # readPrec :: ReadPrec (StateQuantified e) # readListPrec :: ReadPrec [StateQuantified e] #
Show e => Show (StateQuantified e) Source #
Methods showsPrec :: Int -> StateQuantified e -> ShowS # show :: StateQuantified e -> String # showList :: [StateQuantified e] -> ShowS #

parseExpr :: SourceName -> String -> Either ParseError Expr Source #

Parse a CTL expressions from the given string.

The first parameter will be used to identify the source of the text in error messages.

This parser is compatible with the pretty printer of expressions, that is, pretty printed expressions will be parseable by this (unless they contain illegal identifiers for atomic propositions).

Model checking

check :: KripkeStructure String -> Expr -> Int -> Bool Source #

Check if the given expression holds in the given state of the Kripke structure.

satisfyExpr :: KripkeStructure String -> Expr -> [State String] Source #

Obtain all states that satisfy the given CTL expression.

satisfyExpr' :: KripkeStructure String -> Expr -> [Int] Source #

Obtain the identifiers of all states that satisfy the given CTL expression.