hylolib-1.4.0: Tools for hybrid logics related programs

Safe HaskellSafe-Infered

HyLo.Model

Documentation

data Model w n p r Source

Instances

(Ord w, Ord n, Ord p, Ord r) => ModelsRel (Model w n p r, w) (Formula n p r) n p r 
(Read w, Read n, Read p, Read r, Ord w, Ord n, Ord p, Ord r) => Read (Model w n p r) 
(Show w, Show n, Show p, Show r) => Show (Model w n p r) 
(Ord w, Ord n, Ord p, Ord r, Arbitrary w, Arbitrary n, Arbitrary p, Arbitrary r) => Arbitrary (Model w n p r) 
HasSignature (Model w n p r) 
(Ord w, Ord n, Ord p, Ord r) => ModelsRel (Model w n p r) (Formula n p r) n p r 

worlds :: Model w n p r -> Set wSource

succs :: Model w n p r -> r -> w -> Set wSource

valP :: Model w n p r -> p -> Set wSource

valN :: Model w n p r -> n -> wSource

model :: (RelRepr rs r w, ValRepr ps p w, ValNomRepr ns n w) => Set w -> rs -> ps -> ns -> Signature n p r -> Model w n p rSource

equiv :: (Eq w, Eq n, Eq p, Eq r) => Model w n p r -> Model w n p r -> BoolSource

expand :: (Ord n, Ord p, Ord r) => Signature n p r -> Model w n p r -> Model w n p rSource

setSignature :: (Ord n, Ord p, Ord r) => Signature n p r -> Model w n p r -> Model w n p rSource

(??) :: Eq n => Model w n p r -> (n, w) -> Model w n p rSource

removeWorld :: Ord w => w -> Model w n p r -> Model w n p rSource

removeWorlds :: Ord w => Set w -> Model w n p r -> Model w n p rSource

countInModel :: (Ord w, Ord n, Ord p, Ord r) => Formula n p r -> Model w n p r -> IntSource

namesOf :: Eq w => w -> Model w n p r -> [n]Source

propsOf :: Ord w => w -> Model w n p r -> [p]Source

class ModelsRel m f n p r | m -> n, m -> p, m -> r, f -> n, f -> p, f -> r whereSource

Methods

(|=) :: m -> f -> BoolSource

Instances

(Ord r, Ord n, Ord p, ModelsRel (Model n n p r, n) f n p r) => ModelsRel (HerbrandModel n p r, n) f n p r 
(Ord w, Ord n, Ord p, Ord r) => ModelsRel (Model w n p r, w) (Formula n p r) n p r 
(Ord r, Ord n, Ord p, ModelsRel (Model n n p r) f n p r) => ModelsRel (HerbrandModel n p r) f n p r 
(Ord w, Ord n, Ord p, Ord r) => ModelsRel (Model w n p r) (Formula n p r) n p r 

(|/=) :: ModelsRel m f n p r => m -> f -> BoolSource

modelFor :: (HasSignature x, Ord (NomsOf x), Ord (RelsOf x), Ord (PropsOf x)) => x -> Gen (Model Int (NomsOf x) (PropsOf x) (RelsOf x))Source

worldOf :: Model w n p r -> Gen wSource