Safe Haskell	Safe-Inferred
Language	Haskell2010

Language.EFLINT.Spec

Contents

the components of the initial state (all instantiations of TYPE restricted by ENV)
the possible actions performed in a state, only the actions TYPE are enabled

Synopsis

type DomId = String
type Tagged = (Elem, DomId)
data Var = Var DomId String
data Elem
- = String String
- | Int Int
- | Product [Tagged]
data Domain
- = AnyString
- | AnyInt
- | Strings [String]
- | Ints [Int]
- | Products [Var]
- | Time
enumerable :: Spec -> Domain -> Bool
closed_type :: Spec -> DomId -> Maybe Bool
type Arguments = Either [Term] [Modifier]
data Modifier = Rename Var Term
data Kind
- = Fact FactSpec
- | Act ActSpec
- | Duty DutySpec
- | Event EventSpec
data Restriction
- = VarRestriction
- | FunctionRestriction
data TypeSpec = TypeSpec {
- kind :: Kind
- domain :: Domain
- domain_constraint :: Term
- restriction :: Maybe Restriction
- derivation :: [Derivation]
- closed :: Bool
- conditions :: [Term]
}
data Derivation
- = Dv [Var] Term
- | HoldsWhen Term
data FactSpec = FactSpec {
- invariant :: Bool
- actor :: Bool
}
data DutySpec = DutySpec {
- enforcing_acts :: [DomId]
- terminating_acts :: [DomId]
- creating_acts :: [DomId]
- violated_when :: [Term]
}
data ActSpec = ActSpec {
- effects :: [Effect]
- syncs :: [Sync]
- physical :: Bool
}
data Effect
- = CAll [Var] Term
- | TAll [Var] Term
- | OAll [Var] Term
data Sync = Sync [Var] Term
data EventSpec = EventSpec {
- event_effects :: [Effect]
- event_syncs :: [Sync]
}
data Spec = Spec {
- decls :: Map DomId TypeSpec
- aliases :: Map DomId DomId
}
spec_union :: Spec -> Spec -> Spec
decls_union :: Map DomId TypeSpec -> Map DomId TypeSpec -> Map DomId TypeSpec
aliases_union :: Map DomId DomId -> Map DomId DomId -> Map DomId DomId
actor_ref_address :: String
emptySpec :: Spec
basic :: Spec -> Set DomId
derived :: Spec -> Set DomId
is_var :: Spec -> DomId -> Bool
is_function :: Spec -> DomId -> Bool
type Initialiser = [Effect]
emptyInitialiser :: Initialiser
data Statement
- = Trans [Var] TransType (Either Term (DomId, Arguments))
- | Query Term
data TransType
- = Trigger
- | AddEvent
- | RemEvent
- | ObfEvent
type Scenario = [Statement]
data Directive
- = Include FilePath
- | Require FilePath
data Phrase
- = PDo Tagged
- | PTrigger [Var] Term
- | Create [Var] Term
- | Terminate [Var] Term
- | Obfuscate [Var] Term
- | PQuery Term
- | PInstQuery Bool [Var] Term
- | PDeclBlock [Decl]
- | PSkip
data Decl
- = TypeDecl DomId TypeSpec
- | TypeExt DomId [ModClause]
- | PlaceholderDecl DomId DomId
data CDecl
- = CTypeDecl DomId TypeSpec
- | CTypeExt DomId [CModClause]
- | CPlaceholderDecl DomId DomId
isInitialTypeDecl :: Decl -> Bool
extend_spec :: [Decl] -> Spec -> Spec
data ModClause
- = ConditionedByCl [Term]
- | DerivationCl [Derivation]
- | PostCondCl [Effect]
- | SyncCl [Sync]
- | ViolationCl [Term]
- | EnforcingActsCl [DomId]
- | TerminatedByCl [DomId]
- | CreatedByCl [DomId]
data CModClause
- = CConditionedByCl [Term]
- | CDerivationCl [Derivation]
- | CPostCondCl [Effect]
- | CSyncCl [Sync]
- | CViolationCl [Term]
- | CEnforcingActsCl [DomId]
- | CTerminatedByCl [DomId]
- | CCreatedByCl [DomId]
enforcing_act_condition :: DomId -> Term
terminated_by_condition :: DomId -> DomId -> Term
terminated_by_precondition :: DomId -> DomId -> Term
created_by_condition :: DomId -> DomId -> Term
apply_type_ext :: DomId -> [CModClause] -> TypeSpec -> TypeSpec
data CPhrase
- = CDo Tagged
- | CTrigger [Var] Term
- | CCreate [Var] Term
- | CTerminate [Var] Term
- | CObfuscate [Var] Term
- | CQuery Term
- | CInstQuery Bool [Var] Term
- | CPOnlyDecls
- | CPDir CDirective
- | CSeq CPhrase CPhrase
- | CPSkip
data CDirective = DirInv DomId
process_directives :: [CDirective] -> Spec -> Spec
invariants :: Spec -> Set DomId
actors :: Spec -> Set DomId
type Subs = Map Var Tagged
data Term
- = Not Term
- | And Term Term
- | Or Term Term
- | BoolLit Bool
- | Leq Term Term
- | Geq Term Term
- | Ge Term Term
- | Le Term Term
- | Sub Term Term
- | Add Term Term
- | Mult Term Term
- | Mod Term Term
- | Div Term Term
- | IntLit Int
- | StringLit String
- | Eq Term Term
- | Neq Term Term
- | Exists [Var] Term
- | Forall [Var] Term
- | Count [Var] Term
- | Sum [Var] Term
- | Max [Var] Term
- | Min [Var] Term
- | When Term Term
- | Present Term
- | Violated Term
- | Enabled Term
- | Project Term Var
- | Tag Term DomId
- | Untag Term
- | Ref Var
- | App DomId Arguments
- | CurrentTime
data Value
- = ResBool Bool
- | ResString String
- | ResInt Int
- | ResTagged Tagged
data Type
- = TyStrings
- | TyInts
- | TyBool
- | TyTagged DomId
no_decoration :: DomId -> Var
remove_decoration :: Spec -> Var -> DomId
duty_decls :: Spec -> [(DomId, DutySpec)]
trigger_decls :: Spec -> [(DomId, Either EventSpec ActSpec)]
triggerable :: Spec -> DomId -> Bool
find_decl :: Spec -> DomId -> Maybe TypeSpec
find_violation_cond :: Spec -> DomId -> Maybe [Term]
chase_alias :: Spec -> DomId -> DomId
show_arguments :: Arguments -> String
show_modifiers :: [Modifier] -> String
show_projections :: [Var] -> String
show_component :: Tagged -> String
ppTagged :: Tagged -> String
show_stmt :: Statement -> String
valOf :: Tagged -> Elem
tagOf :: Tagged -> DomId
substitutions_of :: [Modifier] -> [(Var, Term)]
make_substitutions_of :: [Var] -> Arguments -> [(Var, Term)]
project :: Tagged -> DomId -> Maybe Tagged
emptySubs :: Subs
subsUnion :: Subs -> Subs -> Subs
subsUnions :: [Subs] -> Subs
type Refiner = Map DomId Domain
emptyRefiner :: Refiner
refine_specification :: Spec -> Refiner -> Spec
actor_decl :: TypeSpec
int_decl :: TypeSpec
ints_decl :: [Int] -> TypeSpec
string_decl :: TypeSpec
strings_decl :: [String] -> TypeSpec
newtype TaggedJSON = TaggedJSON Tagged

Documentation

type DomId = String Source #

type Tagged = (Elem, DomId) Source #

data Var Source #

Constructors

Var DomId String

Instances

Instances details

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

data Elem Source #

Constructors

String String
Int Int
Product [Tagged]

Instances

Instances details

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

data Domain Source #

Constructors

AnyString
AnyInt
Strings [String]
Ints [Int]
Products [Var]
Time

Instances

Instances details

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

enumerable :: Spec -> Domain -> Bool Source #

closed_type :: Spec -> DomId -> Maybe Bool Source #

type Arguments = Either [Term] [Modifier] Source #

data Modifier Source #

Constructors

Rename Var Term

Instances

Instances details

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

data Kind Source #

Constructors

Fact FactSpec
Act ActSpec
Duty DutySpec
Event EventSpec

Instances

Instances details

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

data Restriction Source #

Constructors

VarRestriction
FunctionRestriction

Instances

Instances details

Enum Restriction Source #
Instance details Defined in Language.EFLINT.Spec Methods succ :: Restriction -> Restriction # pred :: Restriction -> Restriction # toEnum :: Int -> Restriction # fromEnum :: Restriction -> Int # enumFrom :: Restriction -> [Restriction] # enumFromThen :: Restriction -> Restriction -> [Restriction] # enumFromTo :: Restriction -> Restriction -> [Restriction] # enumFromThenTo :: Restriction -> Restriction -> Restriction -> [Restriction] #
Read Restriction Source #
Instance details Defined in Language.EFLINT.Spec Methods readsPrec :: Int -> ReadS Restriction # readList :: ReadS [Restriction] # readPrec :: ReadPrec Restriction # readListPrec :: ReadPrec [Restriction] #
Show Restriction Source #
Instance details Defined in Language.EFLINT.Spec Methods showsPrec :: Int -> Restriction -> ShowS # show :: Restriction -> String # showList :: [Restriction] -> ShowS #
Eq Restriction Source #
Instance details Defined in Language.EFLINT.Spec Methods (==) :: Restriction -> Restriction -> Bool # (/=) :: Restriction -> Restriction -> Bool #
Ord Restriction Source #
Instance details Defined in Language.EFLINT.Spec Methods compare :: Restriction -> Restriction -> Ordering # (<) :: Restriction -> Restriction -> Bool # (<=) :: Restriction -> Restriction -> Bool # (>) :: Restriction -> Restriction -> Bool # (>=) :: Restriction -> Restriction -> Bool # max :: Restriction -> Restriction -> Restriction # min :: Restriction -> Restriction -> Restriction #

data TypeSpec Source #

Constructors

TypeSpec
Fields kind :: Kind domain :: Domain domain_constraint :: Term restriction :: Maybe Restriction derivation :: [Derivation] closed :: Bool conditions :: [Term]

Instances

Instances details

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

data Derivation Source #

Constructors

Dv [Var] Term
HoldsWhen Term

Instances

Instances details

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

data FactSpec Source #

Constructors

FactSpec
Fields invariant :: Bool actor :: Bool

Instances

Instances details

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

data DutySpec Source #

Constructors

DutySpec
Fields enforcing_acts :: [DomId] terminating_acts :: [DomId] creating_acts :: [DomId] violated_when :: [Term]

Instances

Instances details

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

data ActSpec Source #

Constructors

ActSpec
Fields effects :: [Effect] syncs :: [Sync] physical :: Bool

Instances

Instances details

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

data Effect Source #

Constructors

CAll [Var] Term
TAll [Var] Term
OAll [Var] Term

Instances

Instances details

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

data Sync Source #

Constructors

Sync [Var] Term

Instances

Instances details

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

data EventSpec Source #

Constructors

EventSpec
Fields event_effects :: [Effect] event_syncs :: [Sync]

Instances

Instances details

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

data Spec Source #

Constructors

Spec
Fields decls :: Map DomId TypeSpec aliases :: Map DomId DomId

Instances

Instances details

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

spec_union :: Spec -> Spec -> Spec Source #

Union of specifications with overrides/replacements, not concretizations

decls_union :: Map DomId TypeSpec -> Map DomId TypeSpec -> Map DomId TypeSpec Source #

Right-based union over type declarations, only replacement, no concretization

aliases_union :: Map DomId DomId -> Map DomId DomId -> Map DomId DomId Source #

actor_ref_address :: String Source #

emptySpec :: Spec Source #

basic :: Spec -> Set DomId Source #

derived :: Spec -> Set DomId Source #

is_var :: Spec -> DomId -> Bool Source #

is_function :: Spec -> DomId -> Bool Source #

the components of the initial state (all instantiations of TYPE restricted by ENV)

the possible actions performed in a state, only the actions TYPE are enabled

type Initialiser = [Effect] Source #

emptyInitialiser :: Initialiser Source #

data Statement Source #

Constructors

Trans [Var] TransType (Either Term (DomId, Arguments))
Query Term

data TransType Source #

Constructors

Trigger
AddEvent
RemEvent
ObfEvent

Instances

Instances details

Enum TransType Source #
Instance details Defined in Language.EFLINT.Spec Methods succ :: TransType -> TransType # pred :: TransType -> TransType # toEnum :: Int -> TransType # fromEnum :: TransType -> Int # enumFrom :: TransType -> [TransType] # enumFromThen :: TransType -> TransType -> [TransType] # enumFromTo :: TransType -> TransType -> [TransType] # enumFromThenTo :: TransType -> TransType -> TransType -> [TransType] #
Show TransType Source #
Instance details Defined in Language.EFLINT.Spec Methods showsPrec :: Int -> TransType -> ShowS # show :: TransType -> String # showList :: [TransType] -> ShowS #
Eq TransType Source #
Instance details Defined in Language.EFLINT.Spec Methods (==) :: TransType -> TransType -> Bool # (/=) :: TransType -> TransType -> Bool #
Ord TransType Source #
Instance details Defined in Language.EFLINT.Spec Methods compare :: TransType -> TransType -> Ordering # (<) :: TransType -> TransType -> Bool # (<=) :: TransType -> TransType -> Bool # (>) :: TransType -> TransType -> Bool # (>=) :: TransType -> TransType -> Bool # max :: TransType -> TransType -> TransType # min :: TransType -> TransType -> TransType #

type Scenario = [Statement] Source #

data Directive Source #

Constructors

Include FilePath
Require FilePath

data Phrase Source #

Constructors

PDo Tagged
PTrigger [Var] Term
Create [Var] Term
Terminate [Var] Term
Obfuscate [Var] Term
PQuery Term
PInstQuery Bool [Var] Term
PDeclBlock [Decl]
PSkip

Instances

Instances details

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

data Decl Source #

Constructors

TypeDecl DomId TypeSpec
TypeExt DomId [ModClause]
PlaceholderDecl DomId DomId

Instances

Instances details

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

data CDecl Source #

Constructors

CTypeDecl DomId TypeSpec
CTypeExt DomId [CModClause]
CPlaceholderDecl DomId DomId

Instances

Instances details

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

isInitialTypeDecl :: Decl -> Bool Source #

extend_spec :: [Decl] -> Spec -> Spec Source #

data ModClause Source #

Constructors

ConditionedByCl [Term]
DerivationCl [Derivation]
PostCondCl [Effect]
SyncCl [Sync]
ViolationCl [Term]
EnforcingActsCl [DomId]
TerminatedByCl [DomId]
CreatedByCl [DomId]

Instances

Instances details

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

data CModClause Source #

Constructors

CConditionedByCl [Term]
CDerivationCl [Derivation]
CPostCondCl [Effect]
CSyncCl [Sync]
CViolationCl [Term]
CEnforcingActsCl [DomId]
CTerminatedByCl [DomId]
CCreatedByCl [DomId]

Instances

Instances details

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

enforcing_act_condition :: DomId -> Term Source #

terminated_by_condition :: DomId -> DomId -> Term Source #

terminated_by_precondition :: DomId -> DomId -> Term Source #

created_by_condition :: DomId -> DomId -> Term Source #

apply_type_ext :: DomId -> [CModClause] -> TypeSpec -> TypeSpec Source #

data CPhrase Source #

Constructors

CDo Tagged
CTrigger [Var] Term
CCreate [Var] Term
CTerminate [Var] Term
CObfuscate [Var] Term
CQuery Term
CInstQuery Bool [Var] Term
CPOnlyDecls
CPDir CDirective
CSeq CPhrase CPhrase
CPSkip

data CDirective Source #

Constructors

DirInv DomId

process_directives :: [CDirective] -> Spec -> Spec Source #

invariants :: Spec -> Set DomId Source #

actors :: Spec -> Set DomId Source #

type Subs = Map Var Tagged Source #

data Term Source #

Constructors

Not Term
And Term Term
Or Term Term
BoolLit Bool
Leq Term Term
Geq Term Term
Ge Term Term
Le Term Term
Sub Term Term
Add Term Term
Mult Term Term
Mod Term Term
Div Term Term
IntLit Int
StringLit String
Eq Term Term
Neq Term Term
Exists [Var] Term
Forall [Var] Term
Count [Var] Term
Sum [Var] Term
Max [Var] Term
Min [Var] Term
When Term Term
Present Term
Violated Term
Enabled Term
Project Term Var
Tag Term DomId
Untag Term
Ref Var
App DomId Arguments
CurrentTime

Instances

Instances details

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

data Value Source #

Constructors

ResBool Bool
ResString String
ResInt Int
ResTagged Tagged

Instances

Instances details

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

data Type Source #

Constructors

TyStrings
TyInts
TyBool
TyTagged DomId

Instances

Instances details

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

no_decoration :: DomId -> Var Source #

remove_decoration :: Spec -> Var -> DomId Source #

duty_decls :: Spec -> [(DomId, DutySpec)] Source #

trigger_decls :: Spec -> [(DomId, Either EventSpec ActSpec)] Source #

triggerable :: Spec -> DomId -> Bool Source #

find_decl :: Spec -> DomId -> Maybe TypeSpec Source #

find_violation_cond :: Spec -> DomId -> Maybe [Term] Source #

chase_alias :: Spec -> DomId -> DomId Source #

show_arguments :: Arguments -> String Source #

show_modifiers :: [Modifier] -> String Source #

show_projections :: [Var] -> String Source #

show_component :: Tagged -> String Source #

ppTagged :: Tagged -> String Source #

show_stmt :: Statement -> String Source #

valOf :: Tagged -> Elem Source #

tagOf :: Tagged -> DomId Source #

substitutions_of :: [Modifier] -> [(Var, Term)] Source #

make_substitutions_of :: [Var] -> Arguments -> [(Var, Term)] Source #

project :: Tagged -> DomId -> Maybe Tagged Source #

emptySubs :: Subs Source #

subsUnion :: Subs -> Subs -> Subs Source #

right-biased

subsUnions :: [Subs] -> Subs Source #

type Refiner = Map DomId Domain Source #

emptyRefiner :: Refiner Source #

refine_specification :: Spec -> Refiner -> Spec Source #

actor_decl :: TypeSpec Source #

int_decl :: TypeSpec Source #

ints_decl :: [Int] -> TypeSpec Source #

string_decl :: TypeSpec Source #

strings_decl :: [String] -> TypeSpec Source #

newtype TaggedJSON Source #

Constructors

TaggedJSON Tagged

Instances

Instances details

ToJSON TaggedJSON Source #
Instance details Defined in Language.EFLINT.Spec Methods toJSON :: TaggedJSON -> Value # toEncoding :: TaggedJSON -> Encoding # toJSONList :: [TaggedJSON] -> Value # toEncodingList :: [TaggedJSON] -> Encoding #