-- Hoogle documentation, generated by Haddock
-- See Hoogle, http://www.haskell.org/hoogle/

-- | Ogma: Runtime Monitor translator: JSON Frontend
--   
--   Ogma is a tool to facilitate the integration of safe runtime monitors
--   into other systems. Ogma extends Copilot, a high-level runtime
--   verification framework that generates hard real-time C99 code.
--   
--   This library contains an abstract representation of an Ogma
--   specification.
@package ogma-spec
@version 1.15.0

-- | Abstract representation of an Ogma specification.
module Data.OgmaSpec

-- | Abstract representation of an Ogma specification.
data Spec a
Spec :: [InternalVariableDef] -> [ExternalVariableDef] -> [Requirement a] -> Spec a
[internalVariables] :: Spec a -> [InternalVariableDef]
[externalVariables] :: Spec a -> [ExternalVariableDef]
[requirements] :: Spec a -> [Requirement a]

-- | Internal variable definition, with a given name, its type and
--   definining expression.
data InternalVariableDef
InternalVariableDef :: String -> String -> String -> InternalVariableDef
[internalVariableName] :: InternalVariableDef -> String
[internalVariableType] :: InternalVariableDef -> String
[internalVariableExpr] :: InternalVariableDef -> String

-- | External variable definition, with a given name and type.
--   
--   The value of external variables is assigned outside Copilot, so they
--   have no defining expression in this type.
data ExternalVariableDef
ExternalVariableDef :: String -> String -> ExternalVariableDef
[externalVariableName] :: ExternalVariableDef -> String
[externalVariableType] :: ExternalVariableDef -> String

-- | Requirement with a given name and a boolean expression.
data Requirement a
Requirement :: String -> a -> String -> Maybe String -> Maybe a -> Requirement a
[requirementName] :: Requirement a -> String
[requirementExpr] :: Requirement a -> a
[requirementDescription] :: Requirement a -> String
[requirementResultType] :: Requirement a -> Maybe String
[requirementResultExpr] :: Requirement a -> Maybe a
instance GHC.Internal.Show.Show Data.OgmaSpec.ExternalVariableDef
instance GHC.Internal.Show.Show Data.OgmaSpec.InternalVariableDef
instance GHC.Internal.Show.Show a => GHC.Internal.Show.Show (Data.OgmaSpec.Requirement a)
instance GHC.Internal.Show.Show a => GHC.Internal.Show.Show (Data.OgmaSpec.Spec a)
