Test.StateMachine.Logic

This module defines a predicate logic-like language and its counterexample semantics.

Documentation

data Logic

Constructors

Bot

Top

Logic :&& Logic

Logic :|| Logic

Logic :=> Logic

Not Logic

LogicPredicate LogicPredicate

Show a => Forall [a] (a -> Logic)

Show a => Exists [a] (a -> Logic)

Boolean Bool

Annotate String Logic

data LogicPredicate

Constructors

(Eq a, Show a) => a :== a

(Eq a, Show a) => a :/= a

(Ord a, Show a) => a :< a

(Ord a, Show a) => a :<= a

(Ord a, Show a) => a :> a

(Ord a, Show a) => a :>= a

(Foldable t, Eq a, Show a, Show (t a)) => Member a (t a)

(Foldable t, Eq a, Show a, Show (t a)) => NotMember a (t a)

Instances

Show LogicPredicate

Defined in Test.StateMachine.Logic

Methods

showsPrec :: Int -> LogicPredicate -> ShowS

show :: LogicPredicate -> String

showList :: [LogicPredicate] -> ShowS

dual :: LogicPredicate -> LogicPredicate

strongNeg :: Logic -> Logic

data Counterexample

Constructors

BotC

Fst Counterexample

Snd Counterexample

EitherC Counterexample Counterexample

ImpliesC Counterexample

NotC Counterexample

PredicateC LogicPredicate

Show a => ForallC a Counterexample

Show a => ExistsC [a] [Counterexample]

BooleanC

AnnotateC String Counterexample

Instances

Show Counterexample

Defined in Test.StateMachine.Logic

Methods

showsPrec :: Int -> Counterexample -> ShowS

show :: Counterexample -> String

showList :: [Counterexample] -> ShowS

data Value

Constructors

VFalse Counterexample

VTrue

Instances

Show Value

Defined in Test.StateMachine.Logic

Methods

showsPrec :: Int -> Value -> ShowS

show :: Value -> String

showList :: [Value] -> ShowS

boolean :: Logic -> Bool

logic :: Logic -> Value

evalLogicPredicate :: LogicPredicate -> Value

gatherAnnotations :: Logic -> [String]

Gather user annotations of a true logic expression.

>>> gatherAnnotations (Top .// "top")
["top"]

>>> gatherAnnotations ((Bot .// "bot") .|| (Top .// "top"))
["top"]

>>> gatherAnnotations (Top .// "top1" .&& Top .// "top2")
["top1","top2"]

>>> gatherAnnotations (Bot .// "bot" .&& Top .// "top")
[]

>>> gatherAnnotations (forall [1,2,3] (\i -> 0 .< i .// "positive"))
["positive","positive","positive"]

>>> gatherAnnotations (forall [0,1,2,3] (\i -> 0 .< i .// "positive"))
[]

>>> gatherAnnotations (exists [1,2,3] (\i -> 0 .< i .// "positive"))
["positive"]

(.==) :: (Eq a, Show a) => a -> a -> Logic infix 5

(./=) :: (Eq a, Show a) => a -> a -> Logic infix 5

(.<) :: (Ord a, Show a) => a -> a -> Logic infix 5

(.<=) :: (Ord a, Show a) => a -> a -> Logic infix 5

(.>) :: (Ord a, Show a) => a -> a -> Logic infix 5

(.>=) :: (Ord a, Show a) => a -> a -> Logic infix 5

member :: (Foldable t, Eq a, Show a, Show (t a)) => a -> t a -> Logic infix 8

notMember :: (Foldable t, Eq a, Show a, Show (t a)) => a -> t a -> Logic infix 8

(.//) :: Logic -> String -> Logic infixl 4

(.&&) :: Logic -> Logic -> Logic infixr 3

(.||) :: Logic -> Logic -> Logic infixr 2

(.=>) :: Logic -> Logic -> Logic infixr 1

forall :: Show a => [a] -> (a -> Logic) -> Logic

exists :: Show a => [a] -> (a -> Logic) -> Logic