Safe Haskell	None
Language	Haskell2010

Language.EFLINT.State

Synopsis

data Info = Info {
- value :: Bool
- from_sat :: Bool
}
data State = State {
- contents :: Map Tagged Info
- time :: Int
}
data Transition = Transition {
- tagged :: Tagged
- exist :: Bool
}
type InputMap = Map Tagged Bool
type Store = Map Tagged Assignment
data Assignment
- = HoldsTrue
- | HoldsFalse
- | Unknown
emptyInput :: InputMap
emptyStore :: Map k a
store_union :: Store -> Store -> Store
store_unions :: [Store] -> Store
make_assignments :: Store -> State -> State
derive :: Tagged -> State -> State
derive_all :: [Tagged] -> State -> State
create :: Tagged -> State -> State
create_all :: [Tagged] -> State -> State
terminate :: Tagged -> State -> State
terminate_all :: [Tagged] -> State -> State
obfuscate :: Tagged -> State -> State
obfuscate_all :: [Tagged] -> State -> State
holds :: Tagged -> State -> Bool
emptyState :: State
increment_time :: State -> State
state_holds :: State -> [Tagged]
state_input_holds :: State -> InputMap -> [Tagged]
state_not_holds :: State -> [Tagged]
input_holds :: InputMap -> [Tagged]
data Context = Context {
- ctx_spec :: Spec
- ctx_state :: State
- ctx_transitions :: [Transition]
- ctx_duties :: [Tagged]
}
emptyContext :: Spec -> Context
data TransInfo = TransInfo {
- trans_tagged :: Tagged
- trans_assignments :: Store
- trans_forced :: Bool
- trans_actor :: Maybe Tagged
- trans_syncs :: [TransInfo]
}
trans_is_action :: TransInfo -> Bool
data Violation
- = DutyViolation Tagged
- | TriggerViolation TransInfo
- | InvariantViolation DomId
data QueryRes
- = QuerySuccess
- | QueryFailure
data Error
- = NotTriggerable Tagged
- | NonDeterministicTransition
- | CompilationError String
- | RuntimeError RuntimeError
data RuntimeError
- = MissingInput Tagged
- | InternalError InternalError
data InternalError
- = EnumerateInfiniteDomain DomId Domain
- | MissingSubstitution Var
- | PrimitiveApplication DomId
- | UndeclaredType DomId
print_error :: Error -> String
print_runtime_error :: RuntimeError -> String
print_internal_error :: InternalError -> String

Documentation

data Info Source #

Constructors

Info
Fields value :: Bool from_sat :: Bool

Instances

Instances details

Eq Info Source #
Instance details Defined in Language.EFLINT.State Methods (==) :: Info -> Info -> Bool # (/=) :: Info -> Info -> Bool #
Read Info Source #
Instance details Defined in Language.EFLINT.State Methods readsPrec :: Int -> ReadS Info # readList :: ReadS [Info] # readPrec :: ReadPrec Info # readListPrec :: ReadPrec [Info] #
Show Info Source #
Instance details Defined in Language.EFLINT.State Methods showsPrec :: Int -> Info -> ShowS # show :: Info -> String # showList :: [Info] -> ShowS #

data State Source #

Constructors

State
Fields contents :: Map Tagged Info time :: Int

Instances

Instances details

Eq State Source #
Instance details Defined in Language.EFLINT.State Methods (==) :: State -> State -> Bool # (/=) :: State -> State -> Bool #
Show State Source #
Instance details Defined in Language.EFLINT.State Methods showsPrec :: Int -> State -> ShowS # show :: State -> String # showList :: [State] -> ShowS #

data Transition Source #

Constructors

Transition
Fields tagged :: Tagged exist :: Bool

Instances

Instances details

Eq Transition Source #
Instance details Defined in Language.EFLINT.State Methods (==) :: Transition -> Transition -> Bool # (/=) :: Transition -> Transition -> Bool #
Ord Transition Source #
Instance details Defined in Language.EFLINT.State Methods compare :: Transition -> Transition -> Ordering # (<) :: Transition -> Transition -> Bool # (<=) :: Transition -> Transition -> Bool # (>) :: Transition -> Transition -> Bool # (>=) :: Transition -> Transition -> Bool # max :: Transition -> Transition -> Transition # min :: Transition -> Transition -> Transition #
Read Transition Source #
Instance details Defined in Language.EFLINT.State Methods readsPrec :: Int -> ReadS Transition # readList :: ReadS [Transition] # readPrec :: ReadPrec Transition # readListPrec :: ReadPrec [Transition] #
Show Transition Source #
Instance details Defined in Language.EFLINT.State Methods showsPrec :: Int -> Transition -> ShowS # show :: Transition -> String # showList :: [Transition] -> ShowS #

type InputMap = Map Tagged Bool Source #

type Store = Map Tagged Assignment Source #

data Assignment Source #

Constructors

HoldsTrue
HoldsFalse
Unknown

Instances

Instances details

Eq Assignment Source #
Instance details Defined in Language.EFLINT.State Methods (==) :: Assignment -> Assignment -> Bool # (/=) :: Assignment -> Assignment -> Bool #
Ord Assignment Source #
Instance details Defined in Language.EFLINT.State Methods compare :: Assignment -> Assignment -> Ordering # (<) :: Assignment -> Assignment -> Bool # (<=) :: Assignment -> Assignment -> Bool # (>) :: Assignment -> Assignment -> Bool # (>=) :: Assignment -> Assignment -> Bool # max :: Assignment -> Assignment -> Assignment # min :: Assignment -> Assignment -> Assignment #
Read Assignment Source #
Instance details Defined in Language.EFLINT.State Methods readsPrec :: Int -> ReadS Assignment # readList :: ReadS [Assignment] # readPrec :: ReadPrec Assignment # readListPrec :: ReadPrec [Assignment] #
Show Assignment Source #
Instance details Defined in Language.EFLINT.State Methods showsPrec :: Int -> Assignment -> ShowS # show :: Assignment -> String # showList :: [Assignment] -> ShowS #

emptyInput :: InputMap Source #

emptyStore :: Map k a Source #

store_union :: Store -> Store -> Store Source #

based union over stores, precedence HoldsTrue > HoldsFalse > Unknown

store_unions :: [Store] -> Store Source #

make_assignments :: Store -> State -> State Source #

derive :: Tagged -> State -> State Source #

derive_all :: [Tagged] -> State -> State Source #

create :: Tagged -> State -> State Source #

create_all :: [Tagged] -> State -> State Source #

terminate :: Tagged -> State -> State Source #

terminate_all :: [Tagged] -> State -> State Source #

obfuscate :: Tagged -> State -> State Source #

obfuscate_all :: [Tagged] -> State -> State Source #

holds :: Tagged -> State -> Bool Source #

assumes the instance of a closed type

emptyState :: State Source #

increment_time :: State -> State Source #

state_holds :: State -> [Tagged] Source #

state_input_holds :: State -> InputMap -> [Tagged] Source #

state_not_holds :: State -> [Tagged] Source #

input_holds :: InputMap -> [Tagged] Source #

data Context Source #

Constructors

Context
Fields ctx_spec :: Spec ctx_state :: State ctx_transitions :: [Transition] ctx_duties :: [Tagged]

emptyContext :: Spec -> Context Source #

data TransInfo Source #

Constructors

TransInfo
Fields trans_tagged :: Tagged trans_assignments :: Store trans_forced :: Bool trans_actor :: Maybe Tagged trans_syncs :: [TransInfo]

Instances

Instances details

Eq TransInfo Source #
Instance details Defined in Language.EFLINT.State Methods (==) :: TransInfo -> TransInfo -> Bool # (/=) :: TransInfo -> TransInfo -> Bool #
Ord TransInfo Source #
Instance details Defined in Language.EFLINT.State Methods compare :: TransInfo -> TransInfo -> Ordering # (<) :: TransInfo -> TransInfo -> Bool # (<=) :: TransInfo -> TransInfo -> Bool # (>) :: TransInfo -> TransInfo -> Bool # (>=) :: TransInfo -> TransInfo -> Bool # max :: TransInfo -> TransInfo -> TransInfo # min :: TransInfo -> TransInfo -> TransInfo #
Read TransInfo Source #
Instance details Defined in Language.EFLINT.State Methods readsPrec :: Int -> ReadS TransInfo # readList :: ReadS [TransInfo] # readPrec :: ReadPrec TransInfo # readListPrec :: ReadPrec [TransInfo] #
Show TransInfo Source #
Instance details Defined in Language.EFLINT.State Methods showsPrec :: Int -> TransInfo -> ShowS # show :: TransInfo -> String # showList :: [TransInfo] -> ShowS #

trans_is_action :: TransInfo -> Bool Source #

data Violation Source #

Constructors

DutyViolation Tagged
TriggerViolation TransInfo
InvariantViolation DomId

Instances

Instances details

Eq Violation Source #
Instance details Defined in Language.EFLINT.State Methods (==) :: Violation -> Violation -> Bool # (/=) :: Violation -> Violation -> Bool #
Ord Violation Source #
Instance details Defined in Language.EFLINT.State Methods compare :: Violation -> Violation -> Ordering # (<) :: Violation -> Violation -> Bool # (<=) :: Violation -> Violation -> Bool # (>) :: Violation -> Violation -> Bool # (>=) :: Violation -> Violation -> Bool # max :: Violation -> Violation -> Violation # min :: Violation -> Violation -> Violation #
Read Violation Source #
Instance details Defined in Language.EFLINT.State Methods readsPrec :: Int -> ReadS Violation # readList :: ReadS [Violation] # readPrec :: ReadPrec Violation # readListPrec :: ReadPrec [Violation] #
Show Violation Source #
Instance details Defined in Language.EFLINT.State Methods showsPrec :: Int -> Violation -> ShowS # show :: Violation -> String # showList :: [Violation] -> ShowS #

data QueryRes Source #

Constructors

QuerySuccess
QueryFailure

Instances

Instances details

Eq QueryRes Source #
Instance details Defined in Language.EFLINT.State Methods (==) :: QueryRes -> QueryRes -> Bool # (/=) :: QueryRes -> QueryRes -> Bool #
Ord QueryRes Source #
Instance details Defined in Language.EFLINT.State Methods compare :: QueryRes -> QueryRes -> Ordering # (<) :: QueryRes -> QueryRes -> Bool # (<=) :: QueryRes -> QueryRes -> Bool # (>) :: QueryRes -> QueryRes -> Bool # (>=) :: QueryRes -> QueryRes -> Bool # max :: QueryRes -> QueryRes -> QueryRes # min :: QueryRes -> QueryRes -> QueryRes #
Read QueryRes Source #
Instance details Defined in Language.EFLINT.State Methods readsPrec :: Int -> ReadS QueryRes # readList :: ReadS [QueryRes] # readPrec :: ReadPrec QueryRes # readListPrec :: ReadPrec [QueryRes] #
Show QueryRes Source #
Instance details Defined in Language.EFLINT.State Methods showsPrec :: Int -> QueryRes -> ShowS # show :: QueryRes -> String # showList :: [QueryRes] -> ShowS #

data Error Source #

Constructors

NotTriggerable Tagged
NonDeterministicTransition
CompilationError String
RuntimeError RuntimeError

Instances

Instances details

Eq Error Source #
Instance details Defined in Language.EFLINT.State Methods (==) :: Error -> Error -> Bool # (/=) :: Error -> Error -> Bool #
Ord Error Source #
Instance details Defined in Language.EFLINT.State Methods compare :: Error -> Error -> Ordering # (<) :: Error -> Error -> Bool # (<=) :: Error -> Error -> Bool # (>) :: Error -> Error -> Bool # (>=) :: Error -> Error -> Bool # max :: Error -> Error -> Error # min :: Error -> Error -> Error #
Read Error Source #
Instance details Defined in Language.EFLINT.State Methods readsPrec :: Int -> ReadS Error # readList :: ReadS [Error] # readPrec :: ReadPrec Error # readListPrec :: ReadPrec [Error] #
Show Error Source #
Instance details Defined in Language.EFLINT.State Methods showsPrec :: Int -> Error -> ShowS # show :: Error -> String # showList :: [Error] -> ShowS #

data RuntimeError Source #

Constructors

MissingInput Tagged
InternalError InternalError

Instances

Instances details

Eq RuntimeError Source #
Instance details Defined in Language.EFLINT.State Methods (==) :: RuntimeError -> RuntimeError -> Bool # (/=) :: RuntimeError -> RuntimeError -> Bool #
Ord RuntimeError Source #
Instance details Defined in Language.EFLINT.State Methods compare :: RuntimeError -> RuntimeError -> Ordering # (<) :: RuntimeError -> RuntimeError -> Bool # (<=) :: RuntimeError -> RuntimeError -> Bool # (>) :: RuntimeError -> RuntimeError -> Bool # (>=) :: RuntimeError -> RuntimeError -> Bool # max :: RuntimeError -> RuntimeError -> RuntimeError # min :: RuntimeError -> RuntimeError -> RuntimeError #
Read RuntimeError Source #
Instance details Defined in Language.EFLINT.State Methods readsPrec :: Int -> ReadS RuntimeError # readList :: ReadS [RuntimeError] # readPrec :: ReadPrec RuntimeError # readListPrec :: ReadPrec [RuntimeError] #
Show RuntimeError Source #
Instance details Defined in Language.EFLINT.State Methods showsPrec :: Int -> RuntimeError -> ShowS # show :: RuntimeError -> String # showList :: [RuntimeError] -> ShowS #

data InternalError Source #

Constructors

EnumerateInfiniteDomain DomId Domain
MissingSubstitution Var
PrimitiveApplication DomId
UndeclaredType DomId

Instances

Instances details

Eq InternalError Source #
Instance details Defined in Language.EFLINT.State Methods (==) :: InternalError -> InternalError -> Bool # (/=) :: InternalError -> InternalError -> Bool #
Ord InternalError Source #
Instance details Defined in Language.EFLINT.State Methods compare :: InternalError -> InternalError -> Ordering # (<) :: InternalError -> InternalError -> Bool # (<=) :: InternalError -> InternalError -> Bool # (>) :: InternalError -> InternalError -> Bool # (>=) :: InternalError -> InternalError -> Bool # max :: InternalError -> InternalError -> InternalError # min :: InternalError -> InternalError -> InternalError #
Read InternalError Source #
Instance details Defined in Language.EFLINT.State Methods readsPrec :: Int -> ReadS InternalError # readList :: ReadS [InternalError] # readPrec :: ReadPrec InternalError # readListPrec :: ReadPrec [InternalError] #
Show InternalError Source #
Instance details Defined in Language.EFLINT.State Methods showsPrec :: Int -> InternalError -> ShowS # show :: InternalError -> String # showList :: [InternalError] -> ShowS #

print_error :: Error -> String Source #

print_runtime_error :: RuntimeError -> String Source #

print_internal_error :: InternalError -> String Source #