| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
Language.EFLINT.Spec
Synopsis
- type DomId = String
- type Tagged = (Elem, DomId)
- data Var = Var DomId String
- data Elem
- data Domain
- enumerable :: Spec -> Domain -> Bool
- closed_type :: Spec -> DomId -> Maybe Bool
- type Arguments = Either [Term] [Modifier]
- data Modifier = Rename Var Term
- data Kind
- data TypeSpec = TypeSpec {
- kind :: Kind
- domain :: Domain
- domain_constraint :: Term
- derivation :: [Derivation]
- closed :: Bool
- conditions :: [Term]
- data Derivation
- data FactSpec = FactSpec {}
- data DutySpec = DutySpec {
- enforcing_acts :: [DomId]
- violated_when :: [Term]
- data ActSpec = ActSpec {}
- data Effect
- data Sync = Sync [Var] Term
- data EventSpec = EventSpec {
- event_effects :: [Effect]
- data Spec = Spec {}
- 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
- type Initialiser = [Effect]
- emptyInitialiser :: Initialiser
- data Statement
- data TransType
- type Scenario = [Statement]
- data Directive
- data Phrase
- data Decl
- introducesName :: Decl -> Bool
- extend_spec :: [Decl] -> Spec -> Spec
- data ModClause
- = ConditionedByCl [Term]
- | DerivationCl [Derivation]
- | PostCondCl [Effect]
- | SyncCl [Sync]
- | ViolationCl [Term]
- | EnforcingActsCl [DomId]
- apply_ext :: DomId -> [ModClause] -> Spec -> Spec
- apply_type_ext :: DomId -> [ModClause] -> TypeSpec -> TypeSpec
- data CPhrase
- 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
- data Type
- 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
Constructors
| TypeSpec | |
Fields
| |
data Derivation Source #
Instances
| Eq Derivation Source # | |
Defined in Language.EFLINT.Spec | |
| Ord Derivation Source # | |
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 # | |
| Read Derivation Source # | |
Defined in Language.EFLINT.Spec Methods readsPrec :: Int -> ReadS Derivation # readList :: ReadS [Derivation] # readPrec :: ReadPrec Derivation # readListPrec :: ReadPrec [Derivation] # | |
| Show Derivation Source # | |
Defined in Language.EFLINT.Spec Methods showsPrec :: Int -> Derivation -> ShowS # show :: Derivation -> String # showList :: [Derivation] -> ShowS # | |
Constructors
| DutySpec | |
Fields
| |
Constructors
| EventSpec | |
Fields
| |
Instances
| Eq EventSpec Source # | |
| Ord EventSpec Source # | |
| Read EventSpec Source # | |
| Show EventSpec Source # | |
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
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 #
Instances
| Enum TransType Source # | |
Defined in Language.EFLINT.Spec Methods succ :: TransType -> TransType # pred :: TransType -> TransType # fromEnum :: TransType -> Int # enumFrom :: TransType -> [TransType] # enumFromThen :: TransType -> TransType -> [TransType] # enumFromTo :: TransType -> TransType -> [TransType] # enumFromThenTo :: TransType -> TransType -> TransType -> [TransType] # | |
| Eq TransType Source # | |
| Ord TransType Source # | |
| Show TransType Source # | |
Constructors
| PDo Tagged | |
| PTrigger [Var] Term | |
| Create [Var] Term | |
| Terminate [Var] Term | |
| Obfuscate [Var] Term | |
| PQuery Term | |
| PDeclBlock [Decl] | |
| PSkip |
introducesName :: Decl -> Bool Source #
Constructors
| ConditionedByCl [Term] | |
| DerivationCl [Derivation] | |
| PostCondCl [Effect] | |
| SyncCl [Sync] | |
| ViolationCl [Term] | |
| EnforcingActsCl [DomId] |
data CDirective Source #
process_directives :: [CDirective] -> Spec -> Spec 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 |
no_decoration :: DomId -> Var Source #
show_arguments :: Arguments -> String Source #
show_modifiers :: [Modifier] -> String Source #
show_projections :: [Var] -> String Source #
show_component :: Tagged -> String Source #
subsUnions :: [Subs] -> Subs Source #
strings_decl :: [String] -> TypeSpec Source #
newtype TaggedJSON Source #
Constructors
| TaggedJSON Tagged |
Instances
| ToJSON TaggedJSON Source # | |
Defined in Language.EFLINT.Spec Methods toJSON :: TaggedJSON -> Value # toEncoding :: TaggedJSON -> Encoding # toJSONList :: [TaggedJSON] -> Value # toEncodingList :: [TaggedJSON] -> Encoding # | |