Test.StateMachine.Logic

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

Documentation

data Logic

Constructors

Bot

Top

Logic :&& Logic infixr 3

Logic :|| Logic infixr 2

Logic :=> Logic infixr 1

Not Logic

Predicate Predicate

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

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

Boolean Bool

Annotate String Logic

data Predicate

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

(Eq a, Show a) => Elem a [a]

(Eq a, Show a) => NotElem a [a]

Instances

Show Predicate

Defined in Test.StateMachine.Logic

Methods

showsPrec :: Int -> Predicate -> ShowS

show :: Predicate -> String

showList :: [Predicate] -> ShowS

dual :: Predicate -> Predicate

strongNeg :: Logic -> Logic

data Counterexample

Constructors

BotC

Fst Counterexample

Snd Counterexample

EitherC Counterexample Counterexample

ImpliesC Counterexample

NotC Counterexample

PredicateC Predicate

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

predicate :: Predicate -> Value

(.==) :: (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

elem :: (Eq a, Show a) => a -> [a] -> Logic infix 5

notElem :: (Eq a, Show a) => a -> [a] -> Logic infix 5

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

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

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