{-# LANGUAGE RecordWildCards, LambdaCase #-}

module Language.EFLINT.Interpreter (Config(..), Program(..), interpreter, initialConfig, rest_disabled, rest_enabled, get_transition, context2config, make_initial_state
                   ,OutputWriter, Output(..), getOutput
                   ,errors, violations, ex_triggers, query_ress, inst_query_ress, missing_inputs
                   ,convert_programs, collapse_programs) where

import Language.EFLINT.Eval
import Language.EFLINT.Spec
import Language.EFLINT.Saturation
import Language.EFLINT.StaticEval (compile_phrase, runStatic) 
import Language.EFLINT.State

import Control.Monad (forM, forM_, when)
import Control.Monad.Writer (Writer, tell, runWriter)
import Control.Applicative (empty)

import qualified Data.Map as M
import qualified Data.Set as S

data Program = Program Phrase 
             | PSeq Program Program
             | ProgramSkip
             deriving (Program -> Program -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Program -> Program -> Bool
$c/= :: Program -> Program -> Bool
== :: Program -> Program -> Bool
$c== :: Program -> Program -> Bool
Eq, Int -> Program -> ShowS
[Program] -> ShowS
Program -> [Char]
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
showList :: [Program] -> ShowS
$cshowList :: [Program] -> ShowS
show :: Program -> [Char]
$cshow :: Program -> [Char]
showsPrec :: Int -> Program -> ShowS
$cshowsPrec :: Int -> Program -> ShowS
Show)

data Config = Config {
        Config -> Spec
cfg_spec          :: Spec
      , Config -> State
cfg_state         :: State 
      , Config -> [Transition]
rest_transitions  :: [Transition] -- (label * enabled?) -- replaced
      , Config -> [Tagged]
rest_duties       :: [Tagged] -- replaced after ever step
      }
      deriving (Config -> Config -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Config -> Config -> Bool
$c/= :: Config -> Config -> Bool
== :: Config -> Config -> Bool
$c== :: Config -> Config -> Bool
Eq)

data Output = ErrorVal Error
            | ExecutedTransition TransInfo 
            | Violation Violation
            | QueryRes QueryRes -- whether query succeed or not 
            | InstQueryRes [Tagged]
            deriving (Output -> Output -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Output -> Output -> Bool
$c/= :: Output -> Output -> Bool
== :: Output -> Output -> Bool
$c== :: Output -> Output -> Bool
Eq, Int -> Output -> ShowS
[Output] -> ShowS
Output -> [Char]
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
showList :: [Output] -> ShowS
$cshowList :: [Output] -> ShowS
show :: Output -> [Char]
$cshow :: Output -> [Char]
showsPrec :: Int -> Output -> ShowS
$cshowsPrec :: Int -> Output -> ShowS
Show, ReadPrec [Output]
ReadPrec Output
Int -> ReadS Output
ReadS [Output]
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
readListPrec :: ReadPrec [Output]
$creadListPrec :: ReadPrec [Output]
readPrec :: ReadPrec Output
$creadPrec :: ReadPrec Output
readList :: ReadS [Output]
$creadList :: ReadS [Output]
readsPrec :: Int -> ReadS Output
$creadsPrec :: Int -> ReadS Output
Read)

convert_programs :: [Phrase] -> [Program]
convert_programs :: [Phrase] -> [Program]
convert_programs [Phrase]
phrases = forall a b. (a -> b) -> [a] -> [b]
map Phrase -> Program
Program [Phrase]
phrases

collapse_programs :: [Program] -> Program
collapse_programs :: [Program] -> Program
collapse_programs [] = Program
ProgramSkip
collapse_programs [Program]
programs = (forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldr1 Program -> Program -> Program
PSeq [Program]
programs)

interpreter :: (InputMap, Program) -> Config -> OutputWriter (Maybe Config)
interpreter :: (InputMap, Program) -> Config -> OutputWriter (Maybe Config)
interpreter (InputMap
inpm, Program Phrase
p) Config
cfg = case forall a. M_Stc a -> Spec -> Either [[Char]] (Spec, a)
runStatic (Phrase -> M_Stc CPhrase
compile_phrase Phrase
p) (Context -> Spec
ctx_spec Context
ctx) of
    Left [[Char]]
err  -> forall w (m :: * -> *). MonadWriter w m => w -> m ()
tell [Error -> Output
ErrorVal ([Char] -> Error
CompilationError ([[Char]] -> [Char]
unlines [[Char]]
err))] forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Maybe a
Nothing 
    Right (Spec
spec', CPhrase
p') -> forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Context -> Config
context2config forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> CPhrase -> InputMap -> Context -> OutputWriter (Maybe Context)
sem_phrase CPhrase
p' InputMap
inpm 
                          (Context
ctx{ctx_spec :: Spec
ctx_spec = Spec
spec', ctx_state :: State
ctx_state = Spec -> State -> State
rebase_and_sat Spec
spec' (Context -> State
ctx_state Context
ctx)}) 
  where ctx :: Context
ctx = Config -> Context
config2context Config
cfg
interpreter (InputMap
inpm, PSeq Program
p1 Program
p2) Config
cfg = ((InputMap, Program) -> Config -> OutputWriter (Maybe Config)
interpreter (InputMap
inpm,Program
p1) Config
cfg) forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= (InputMap, Program) -> Config -> OutputWriter (Maybe Config)
interpreter (InputMap
inpm,Program
p2) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall b a. b -> (a -> b) -> Maybe a -> b
maybe Config
cfg forall a. a -> a
id
interpreter (InputMap
inpm, Program
ProgramSkip) Config
cfg = forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Maybe a
Nothing

initialConfig :: Maybe (Spec, State) -> Config
initialConfig Maybe (Spec, State)
Nothing = Context -> Config
context2config (Spec -> Context
emptyContext Spec
emptySpec)
initialConfig (Just (Spec
spec,State
state)) = Context -> Config
context2config forall a b. (a -> b) -> a -> b
$
  (Spec -> Context
emptyContext Spec
spec) { ctx_state :: State
ctx_state = State
state }

context2config :: Context -> Config
context2config :: Context -> Config
context2config Context
ctx = Config {
    cfg_spec :: Spec
cfg_spec    = Context -> Spec
ctx_spec Context
ctx
  , cfg_state :: State
cfg_state   = Context -> State
ctx_state Context
ctx
  , rest_transitions :: [Transition]
rest_transitions = Context -> [Transition]
ctx_transitions Context
ctx
  , rest_duties :: [Tagged]
rest_duties      = Context -> [Tagged]
ctx_duties Context
ctx
  }

config2context :: Config -> Context
config2context :: Config -> Context
config2context Config
cfg = Context {
    ctx_spec :: Spec
ctx_spec = Config -> Spec
cfg_spec Config
cfg
  , ctx_state :: State
ctx_state = Config -> State
cfg_state Config
cfg
  , ctx_transitions :: [Transition]
ctx_transitions = []
  , ctx_duties :: [Tagged]
ctx_duties = []
  }

rest_enabled :: Config -> [Tagged]
rest_enabled = forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> a
fst forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. (a -> Bool) -> [a] -> [a]
filter forall a b. (a, b) -> b
snd forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map Transition -> (Tagged, Bool)
get_transition forall b c a. (b -> c) -> (a -> b) -> a -> c
. Config -> [Transition]
rest_transitions
rest_disabled :: Config -> [Tagged]
rest_disabled = forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> a
fst forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> b
snd) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map Transition -> (Tagged, Bool)
get_transition forall b c a. (b -> c) -> (a -> b) -> a -> c
. Config -> [Transition]
rest_transitions

get_transition :: Transition -> (Tagged, Bool)
get_transition :: Transition -> (Tagged, Bool)
get_transition Transition
transition = (Transition -> Tagged
tagged Transition
transition, Transition -> Bool
exist Transition
transition)

ex_triggers :: [Output] -> [TransInfo]
ex_triggers :: [Output] -> [TransInfo]
ex_triggers = forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Output -> [TransInfo]
op
 where op :: Output -> [TransInfo]
op (ExecutedTransition TransInfo
out) = [TransInfo
out]
       op Output
_ = []

violations :: [Output] -> [Violation]
violations :: [Output] -> [Violation]
violations = forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Output -> [Violation]
op
 where op :: Output -> [Violation]
op (Violation Violation
v) = [Violation
v]
       op Output
_ = []

errors :: [Output] -> [Error]
errors :: [Output] -> [Error]
errors = forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Output -> [Error]
op
  where op :: Output -> [Error]
op (ErrorVal Error
err) = [Error
err]
        op Output
_ = []

query_ress :: [Output] -> [QueryRes]
query_ress :: [Output] -> [QueryRes]
query_ress = forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Output -> [QueryRes]
op
  where op :: Output -> [QueryRes]
op (QueryRes QueryRes
b) = [QueryRes
b]
        op Output
_ = []

inst_query_ress :: [Output] -> [[Tagged]]
inst_query_ress :: [Output] -> [[Tagged]]
inst_query_ress = forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Output -> [[Tagged]]
op
  where op :: Output -> [[Tagged]]
op (InstQueryRes [Tagged]
vs) = [[Tagged]
vs]
        op Output
_                 = []

missing_inputs :: [Output] -> [Tagged]
missing_inputs :: [Output] -> [Tagged]
missing_inputs = forall a. Set a -> [a]
S.toList forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Ord a => [a] -> Set a
S.fromList forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Output -> [Tagged]
op
  where op :: Output -> [Tagged]
op (ErrorVal (RuntimeError (MissingInput Tagged
te))) = [Tagged
te]
        op Output
_ = []

type OutputWriter = Writer [Output]

getOutput :: OutputWriter a -> (a,[Output])
getOutput :: forall a. OutputWriter a -> (a, [Output])
getOutput = forall w a. Writer w a -> (a, w)
runWriter

error_or_process :: M_Subs a -> Spec -> State -> InputMap -> ([a] -> OutputWriter (Maybe Context)) -> OutputWriter (Maybe Context)
error_or_process :: forall a.
M_Subs a
-> Spec
-> State
-> InputMap
-> ([a] -> OutputWriter (Maybe Context))
-> OutputWriter (Maybe Context)
error_or_process M_Subs a
ma Spec
spec State
state InputMap
inpm [a] -> OutputWriter (Maybe Context)
fa = case forall a.
M_Subs a
-> Spec -> State -> InputMap -> Subs -> Either RuntimeError [a]
runSubs M_Subs a
ma Spec
spec State
state InputMap
inpm Subs
emptySubs of
  Left RuntimeError
err  -> forall w (m :: * -> *). MonadWriter w m => w -> m ()
tell [Error -> Output
ErrorVal forall a b. (a -> b) -> a -> b
$ RuntimeError -> Error
RuntimeError RuntimeError
err] forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Maybe a
Nothing
  Right [a]
as  -> [a] -> OutputWriter (Maybe Context)
fa [a]
as

sem_phrase :: CPhrase -> InputMap -> Context -> OutputWriter (Maybe Context)
sem_phrase :: CPhrase -> InputMap -> Context -> OutputWriter (Maybe Context)
sem_phrase CPhrase
p InputMap
inpm Context
c0 = case CPhrase
p of
  CPhrase
CPSkip   -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Maybe a
Nothing
  CPhrase
CPOnlyDecls -> OutputWriter (Maybe Context)
no_effect 
  CQuery Term
t -> forall a.
M_Subs a
-> Spec
-> State
-> InputMap
-> ([a] -> OutputWriter (Maybe Context))
-> OutputWriter (Maybe Context)
error_or_process (Term -> M_Subs Value
eval Term
t) Spec
spec State
state InputMap
inpm forall a b. (a -> b) -> a -> b
$ \[Value]
vs -> do  
                 let queryRes :: QueryRes
queryRes | forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (forall a. Eq a => a -> a -> Bool
== (Bool -> Value
ResBool Bool
True)) [Value]
vs = QueryRes
QuerySuccess
                              | Bool
otherwise                  = QueryRes
QueryFailure
                 forall w (m :: * -> *). MonadWriter w m => w -> m ()
tell [QueryRes -> Output
QueryRes QueryRes
queryRes] forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> OutputWriter (Maybe Context)
no_effect
  CInstQuery Bool
b [Var]
vs Term
t -> 
    let t' :: Term
t' | Bool
b         = Term -> Term -> Term
When Term
t (Term -> Term
Present Term
t)
           | Bool
otherwise = Term
t
    in forall a.
M_Subs a
-> Spec
-> State
-> InputMap
-> ([a] -> OutputWriter (Maybe Context))
-> OutputWriter (Maybe Context)
error_or_process (forall a. [Var] -> M_Subs a -> M_Subs [a]
foreach [Var]
vs (forall a. M_Subs Value -> (Tagged -> M_Subs a) -> M_Subs a
whenTagged (Term -> M_Subs Value
eval Term
t') forall (m :: * -> *) a. Monad m => a -> m a
return)) Spec
spec State
state InputMap
inpm forall a b. (a -> b) -> a -> b
$ \[[Tagged]]
vs -> 
                      forall w (m :: * -> *). MonadWriter w m => w -> m ()
tell [[Tagged] -> Output
InstQueryRes (forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[Tagged]]
vs)] forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> OutputWriter (Maybe Context)
no_effect
  CCreate [Var]
vs Term
t    -> Effect -> OutputWriter (Maybe Context)
single_effect ([Var] -> Term -> Effect
CAll [Var]
vs Term
t)
  CTerminate [Var]
vs Term
t -> Effect -> OutputWriter (Maybe Context)
single_effect ([Var] -> Term -> Effect
TAll [Var]
vs Term
t)
  CObfuscate [Var]
vs Term
t -> Effect -> OutputWriter (Maybe Context)
single_effect ([Var] -> Term -> Effect
OAll [Var]
vs Term
t)
  CDo Tagged
te          -> forall a.
M_Subs a
-> Spec
-> State
-> InputMap
-> ([a] -> OutputWriter (Maybe Context))
-> OutputWriter (Maybe Context)
error_or_process (Tagged -> M_Subs (Either [Char] [TransInfo])
trigger_or_fail Tagged
te) Spec
spec State
state InputMap
inpm [Either [Char] [TransInfo]] -> OutputWriter (Maybe Context)
consider_transinfos
  CTrigger [Var]
vs Term
t -> let m_subs :: M_Subs (Either [Char] [TransInfo])
m_subs = do  
                        [Tagged]
tes <- forall a. [Var] -> M_Subs a -> M_Subs [a]
foreach [Var]
vs (forall a. M_Subs Value -> (Tagged -> M_Subs a) -> M_Subs a
whenTagged (Term -> M_Subs Value
eval Term
t) forall (m :: * -> *) a. Monad m => a -> m a
return)
                        case [Tagged]
tes of 
                         (te :: Tagged
te@(Elem
_,[Char]
d):[Tagged]
_) | Spec -> [Char] -> Bool
triggerable Spec
spec [Char]
d -> forall a b. b -> Either a b
Right forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [Tagged]
tes Tagged -> M_Subs TransInfo
instantiate_trans 
                                      | Bool
otherwise -> forall (m :: * -> *) a. Monad m => a -> m a
return (forall a b. a -> Either a b
Left [Char]
d)
                         [Tagged]
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return (forall a b. b -> Either a b
Right [])
                     in forall a.
M_Subs a
-> Spec
-> State
-> InputMap
-> ([a] -> OutputWriter (Maybe Context))
-> OutputWriter (Maybe Context)
error_or_process M_Subs (Either [Char] [TransInfo])
m_subs Spec
spec State
state InputMap
inpm [Either [Char] [TransInfo]] -> OutputWriter (Maybe Context)
consider_transinfos
  CPDir CDirective
dir -> Store -> [CDirective] -> OutputWriter (Maybe Context)
return_context forall {k} {a}. Map k a
emptyStore [CDirective
dir] 
  CSeq CPhrase
p CPhrase
q -> CPhrase -> InputMap -> Context -> OutputWriter (Maybe Context)
sem_phrase CPhrase
p InputMap
inpm Context
c0 forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= (CPhrase -> InputMap -> Context -> OutputWriter (Maybe Context)
sem_phrase CPhrase
q InputMap
inpm forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall b a. b -> (a -> b) -> Maybe a -> b
maybe Context
c0 forall a. a -> a
id)
  where spec :: Spec
spec = Context -> Spec
ctx_spec Context
c0
        state :: State
state = Context -> State
ctx_state Context
c0

        return_context :: Store -> [CDirective] -> OutputWriter (Maybe Context)
        return_context :: Store -> [CDirective] -> OutputWriter (Maybe Context)
return_context Store
ass [CDirective]
dirs = do  
          let duties :: [Tagged]
duties = [ Tagged
te | te :: Tagged
te@(Elem
v,[Char]
d) <- (State -> InputMap -> [Tagged]
state_input_holds State
state' InputMap
inpm)
                            , Duty DutySpec
_ <- forall b a. b -> (a -> b) -> Maybe a -> b
maybe [] (forall a. a -> [a] -> [a]
:[]) (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap TypeSpec -> Kind
kind (Spec -> [Char] -> Maybe TypeSpec
find_decl Spec
spec' [Char]
d)) ]
          forall a.
M_Subs a
-> Spec
-> State
-> InputMap
-> ([a] -> OutputWriter (Maybe Context))
-> OutputWriter (Maybe Context)
error_or_process ([Tagged] -> M_Subs [Violation]
find_duty_violations [Tagged]
duties) Spec
spec' State
state' InputMap
inpm forall a b. (a -> b) -> a -> b
$ \[[Violation]]
d_viols -> 
            forall a.
M_Subs a
-> Spec
-> State
-> InputMap
-> ([a] -> OutputWriter (Maybe Context))
-> OutputWriter (Maybe Context)
error_or_process ([[Char]] -> M_Subs [Violation]
find_inv_violations (forall a. Set a -> [a]
S.toList forall a b. (a -> b) -> a -> b
$ Spec -> Set [Char]
invariants Spec
spec')) Spec
spec' State
state' InputMap
inpm forall a b. (a -> b) -> a -> b
$ \[[Violation]]
i_viols -> do
              forall w (m :: * -> *). MonadWriter w m => w -> m ()
tell (forall a b. (a -> b) -> [a] -> [b]
map Violation -> Output
Violation (forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[Violation]]
d_viols forall a. [a] -> [a] -> [a]
++ forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[Violation]]
i_viols)) 
              forall a.
M_Subs a
-> Spec
-> State
-> InputMap
-> ([a] -> OutputWriter (Maybe Context))
-> OutputWriter (Maybe Context)
error_or_process M_Subs [Transition]
find_transitions Spec
spec' State
state' InputMap
inpm forall a b. (a -> b) -> a -> b
$ \[[Transition]]
tss ->  
                forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ Context
c0
                  { ctx_state :: State
ctx_state = State
state'
                  , ctx_spec :: Spec
ctx_spec = Spec
spec'
                  , ctx_transitions :: [Transition]
ctx_transitions = forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[Transition]]
tss
                  , ctx_duties :: [Tagged]
ctx_duties = [Tagged]
duties 
                  }
          where state' :: State
state' = Spec -> State -> State
rebase_and_sat Spec
spec (Spec -> Store -> State -> State
make_assignments Spec
spec' Store
ass State
state)
                spec' :: Spec
spec'  = [CDirective] -> Spec -> Spec
process_directives [CDirective]
dirs Spec
spec

        no_effect :: OutputWriter (Maybe Context)
        no_effect :: OutputWriter (Maybe Context)
no_effect = Store -> [CDirective] -> OutputWriter (Maybe Context)
return_context forall {k} {a}. Map k a
emptyStore []

        single_effect :: Effect -> OutputWriter (Maybe Context)
        single_effect :: Effect -> OutputWriter (Maybe Context)
single_effect Effect
eff =
          forall a.
M_Subs a
-> Spec
-> State
-> InputMap
-> ([a] -> OutputWriter (Maybe Context))
-> OutputWriter (Maybe Context)
error_or_process (Effect -> M_Subs Store
eval_effect Effect
eff) Spec
spec State
state InputMap
inpm forall a b. (a -> b) -> a -> b
$ \[Store]
stores ->
            Store -> [CDirective] -> OutputWriter (Maybe Context)
return_context (forall (f :: * -> *) k a.
(Foldable f, Ord k) =>
f (Map k a) -> Map k a
M.unions [Store]
stores) {- always just one store-} []

        trigger_or_fail :: Tagged -> M_Subs (Either DomId [TransInfo])
        trigger_or_fail :: Tagged -> M_Subs (Either [Char] [TransInfo])
trigger_or_fail te :: Tagged
te@(Elem
_,[Char]
d) | Spec -> [Char] -> Bool
triggerable Spec
spec [Char]
d = forall a b. b -> Either a b
Right forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall a. a -> [a] -> [a]
:[]) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Tagged -> M_Subs TransInfo
instantiate_trans Tagged
te
                                 | Bool
otherwise          = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a b. a -> Either a b
Left [Char]
d 

        consider_transinfos :: [Either [Char] [TransInfo]] -> OutputWriter (Maybe Context)
consider_transinfos [Left [Char]
d] = forall w (m :: * -> *). MonadWriter w m => w -> m ()
tell [Error -> Output
ErrorVal ([Char] -> Error
NotTriggerable [Char]
d)] forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> OutputWriter (Maybe Context)
no_effect
        consider_transinfos [Right [TransInfo]
infos] = do
          forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [TransInfo]
infos forall a b. (a -> b) -> a -> b
$ \TransInfo
info -> do  forall w (m :: * -> *). MonadWriter w m => w -> m ()
tell [TransInfo -> Output
ExecutedTransition TransInfo
info]
                                     TransInfo -> WriterT [Output] Identity ()
tell_violations TransInfo
info
          Store -> [CDirective] -> OutputWriter (Maybe Context)
return_context ([Store] -> Store
store_unions (forall a b. (a -> b) -> [a] -> [b]
map TransInfo -> Store
trans_assignments [TransInfo]
infos)) [] 
        consider_transinfos [Either [Char] [TransInfo]]
_ = forall a. HasCallStack => [Char] -> a
error [Char]
"ASSERT: consider_transinfos"

tell_violations :: TransInfo -> OutputWriter ()
tell_violations :: TransInfo -> WriterT [Output] Identity ()
tell_violations TransInfo
info 
  | TransInfo -> Bool
trans_is_action TransInfo
info = 
      -- report whether this action is violated (potentially caused by any successor)
      -- if not violated, then so will not any successor
      forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (TransInfo -> Bool
trans_forced TransInfo
info) (forall w (m :: * -> *). MonadWriter w m => w -> m ()
tell [Violation -> Output
Violation (TransInfo -> Violation
TriggerViolation TransInfo
info)])
  | Bool
otherwise = 
      -- report whether successors are violated, given that they could be actions
      forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ TransInfo -> WriterT [Output] Identity ()
tell_violations (TransInfo -> [TransInfo]
trans_syncs TransInfo
info) 

find_inv_violations :: [DomId] -> M_Subs [Violation]
find_inv_violations :: [[Char]] -> M_Subs [Violation]
find_inv_violations [[Char]]
ds = do 
  Spec
spec <- M_Subs Spec
get_spec 
  forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [[Char]]
ds forall a b. (a -> b) -> a -> b
$ \[Char]
d -> do
    let term :: Term
term = [Var] -> Term -> Term
Exists [[Char] -> [Char] -> Var
Var [Char]
d [Char]
""] (Term -> Term
Present (Var -> Term
Ref ([Char] -> [Char] -> Var
Var [Char]
d [Char]
"")))
    forall a. M_Subs a -> M_Subs a
ignoreMissingInput (M_Subs Value -> M_Subs ()
checkFalse (Term -> M_Subs Value
eval Term
term))
    forall (m :: * -> *) a. Monad m => a -> m a
return ([Char] -> Violation
InvariantViolation [Char]
d)

find_duty_violations :: [Tagged] -> M_Subs [Violation]
find_duty_violations :: [Tagged] -> M_Subs [Violation]
find_duty_violations [Tagged]
tes = do 
  Spec
spec <- M_Subs Spec
get_spec 
  forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [Tagged]
tes forall a b. (a -> b) -> a -> b
$ \te :: Tagged
te@(Elem
_,[Char]
d) -> do
    forall a. M_Subs a -> M_Subs a
ignoreMissingInput (Tagged -> Maybe [Term] -> M_Subs Bool
eval_violation_condition Tagged
te (Spec -> [Char] -> Maybe [Term]
find_violation_cond Spec
spec [Char]
d)) forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case 
      Bool
True  -> forall (m :: * -> *) a. Monad m => a -> m a
return (Tagged -> Violation
DutyViolation Tagged
te)
      Bool
False -> forall (f :: * -> *) a. Alternative f => f a
empty 
 
find_transitions :: M_Subs [Transition]
find_transitions :: M_Subs [Transition]
find_transitions = do
  Spec
spec <- M_Subs Spec
get_spec 
  forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM forall {b}. ([Char], b) -> M_Subs [Transition]
gen_trans (Spec -> [([Char], Either EventSpec ActSpec)]
trigger_decls Spec
spec)
  where gen_trans :: ([Char], b) -> M_Subs [Transition]
gen_trans ([Char]
d,b
_) = forall a. M_Subs a -> M_Subs [a]
results forall a b. (a -> b) -> a -> b
$ forall a. M_Subs a -> M_Subs a
ignoreMissingInput forall a b. (a -> b) -> a -> b
$ do
          Tagged
tagged <- Var -> M_Subs Tagged
every_possible_subs ([Char] -> Var
no_decoration [Char]
d)
          Bool
exist  <- Tagged -> M_Subs Bool
is_in_virtual_state Tagged
tagged
          forall (m :: * -> *) a. Monad m => a -> m a
return Transition{Bool
Tagged
exist :: Bool
tagged :: Tagged
exist :: Bool
tagged :: Tagged
..}

every_possible_subs :: Var -> M_Subs Tagged
every_possible_subs :: Var -> M_Subs Tagged
every_possible_subs Var
x = do
    Spec
spec <- M_Subs Spec
get_spec
    let d :: [Char]
d = Spec -> Var -> [Char]
remove_decoration Spec
spec Var
x
    (Domain
dom, Term
_) <- [Char] -> M_Subs (Domain, Term)
get_dom [Char]
d
    if Spec -> Domain -> Bool
enumerable Spec
spec Domain
dom then [Char] -> M_Subs Tagged
generate_instances [Char]
d
                           else [Char] -> M_Subs Tagged
every_available_subs [Char]
d
 where generate_instances :: [Char] -> M_Subs Tagged
generate_instances [Char]
d = do
          (Domain
dom, Term
dom_filter) <- [Char] -> M_Subs (Domain, Term)
get_dom [Char]
d
          Elem
e <- [Char] -> Domain -> M_Subs Elem
instantiate_domain [Char]
d Domain
dom
          let bindings :: Subs
bindings = case (Domain
dom,Elem
e) of (Products [Var]
xs, Product [Tagged]
args) -> forall k a. Ord k => [(k, a)] -> Map k a
M.fromList (forall a b. [a] -> [b] -> [(a, b)]
zip [Var]
xs [Tagged]
args)
                                         (Domain, Elem)
_ -> forall k a. k -> a -> Map k a
M.singleton ([Char] -> Var
no_decoration [Char]
d) (Elem
e,[Char]
d) 
          forall a. (Subs -> Subs) -> M_Subs a -> M_Subs a
modify_subs (Subs -> Subs -> Subs
`subsUnion` Subs
bindings) (M_Subs Value -> M_Subs ()
checkTrue (Term -> M_Subs Value
eval Term
dom_filter))
          forall (m :: * -> *) a. Monad m => a -> m a
return (Elem
e,[Char]
d)
       every_available_subs :: [Char] -> M_Subs Tagged
every_available_subs [Char]
d = do
          (Domain
dom, Term
dom_filter) <- [Char] -> M_Subs (Domain, Term)
get_dom [Char]
d
          case Domain
dom of
            Products [Var]
xs -> do
              [Tagged]
args <- forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence (forall a b. (a -> b) -> [a] -> [b]
map Var -> M_Subs Tagged
every_possible_subs [Var]
xs)
              forall a. (Subs -> Subs) -> M_Subs a -> M_Subs a
modify_subs (Subs -> Subs -> Subs
`subsUnion` (forall k a. Ord k => [(k, a)] -> Map k a
M.fromList (forall a b. [a] -> [b] -> [(a, b)]
zip [Var]
xs [Tagged]
args))) (M_Subs Value -> M_Subs ()
checkTrue (Term -> M_Subs Value
eval Term
dom_filter))
              forall (m :: * -> *) a. Monad m => a -> m a
return ([Tagged] -> Elem
Product [Tagged]
args, [Char]
d)
            Domain
_ -> do
              State
state <- M_Subs State
get_state
              InputMap
input <- M_Subs InputMap
get_input
              forall a. [a] -> M_Subs a
nd forall a b. (a -> b) -> a -> b
$  [ Tagged
te | te :: Tagged
te@(Elem
v,[Char]
d') <- State -> InputMap -> [Tagged]
state_input_holds State
state InputMap
input, [Char]
d' forall a. Eq a => a -> a -> Bool
== [Char]
d ]

make_initial_state :: Spec -> Initialiser -> State
make_initial_state :: Spec -> Initialiser -> State
make_initial_state Spec
spec Initialiser
inits = do
  case forall a.
M_Subs a
-> Spec -> State -> InputMap -> Subs -> Either RuntimeError [a]
runSubs ([Store] -> Store
store_unions forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Effect -> M_Subs Store
eval_effect Initialiser
inits) Spec
spec State
emptyState InputMap
emptyInput Subs
emptySubs of
    Left RuntimeError
err -> forall a. HasCallStack => [Char] -> a
error (RuntimeError -> [Char]
print_runtime_error RuntimeError
err)
    Right [Store]
res -> case [Store]
res of 
      []    -> forall a. HasCallStack => [Char] -> a
error [Char]
"failed to initialise state"
      [Store
sto] -> Spec -> State -> State
rebase_and_sat Spec
spec (Spec -> Store -> State -> State
make_assignments Spec
spec Store
sto State
emptyState)
      [Store]
_     -> forall a. HasCallStack => [Char] -> a
error [Char]
"non-deterministic state initialisation"