Test.StateMachine.Logic

This module provides a propositional logic which gives counterexamples when the proposition is false.

Documentation

data Logic

Constructors

Bot

Top

Logic :&& Logic infixr 3

Logic :|| Logic infixr 2

Logic :=> Logic infixr 1

Not Logic

Predicate Predicate

Annotate String Logic

Instances

Show Logic

Methods

showsPrec :: Int -> Logic -> ShowS

show :: Logic -> String

showList :: [Logic] -> ShowS

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

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

AnnotateC String Counterexample

Instances

Show Counterexample

Methods

showsPrec :: Int -> Counterexample -> ShowS

show :: Counterexample -> String

showList :: [Counterexample] -> ShowS

data Value

Constructors

VFalse Counterexample

VTrue

Instances

Show Value

Methods

showsPrec :: Int -> Value -> ShowS

show :: Value -> String

showList :: [Value] -> ShowS

logic :: Logic -> Value

predicate :: Predicate -> Value