
 TorXakis - Model Based Testing 
 Copyright ( c ) 2015 - 2017 TNO and Radboud University 
 See LICENSE at root directory of this repository . 

TorXakis - Model Based Testing
Copyright (c) 2015-2017 TNO and Radboud University
See LICENSE at root directory of this repository.
-}


# LANGUAGE FlexibleInstances #
  | TorXakis Core Environment ( Internal State ) Data Type Definitions .
module EnvCore
  IOC = StateT EnvC IO
                  -- torxakis core main state monad transformer
  , EnvC(..)
  , CoreState(..)
  : : String - > IOC SMTData . SmtEnv
  : : String - > SMTData . SmtEnv - > IOC ( )
  , getParams -- :: [String] -> IOC [(String,String)]
  , setParams -- :: [(String,String)] -> IOC [(String,String)]
  , initUnid -- :: IOC.IOC Int
  , newUnid -- :: IOC.IOC Int
  , putMsgs -- :: [EnvData.Msg] -> IOC ()
  , putInfo -- :: [String] -> IOC ()
  -- * Operation on core-state
  , modifyCS
  , putCS
  , incUnid
  )
where

import           Control.Monad.State hiding (state)

import qualified Data.Map            as Map


-- import from local
import           Config    hiding (setParams)
import qualified EnvBasic    as EnvB
import qualified EnvData
import qualified ParamCore

  import from behavedefs
import qualified BTree

  import from defs
import qualified Sigs
import qualified TxsDDefs
import qualified TxsDefs

  import from valexpr
import           Id
import qualified VarId               (VarId)
import           Name

-- import from solve
import qualified SMTData

-- ----------------------------------------------------------------------------------------- --
  IOC :   torxakis core state monad transformer

type  IOC  = StateT EnvC IO

   ( StateT IOC.EnvC IO )
  where
     newUnid  =  newUnid
     putMsgs  =  putMsgs
     setChanoffers = setChanoffers
     getChanoffers = getChanoffers
 

data EnvC = EnvC
  { config :: Config           -- ^ Core configuration.
  , unid   :: Id               -- ^ Last used unique number.
  , params :: ParamCore.Params
  , state  :: CoreState        -- ^ State specific information.
  }

data CoreState = Noning
  named smt solver envs
  TorXakis definitions
  TorXakis signatures
                        , putmsgs :: [EnvData.Msg] -> IOC ()       -- (error) reporting
                        , chanoffers :: Map.Map (Name, Int) VarId.VarId    -- substitution for channel offers (LPE translation)
                        }
  named smt solver envs
  TorXakis definitions
  TorXakis signatures
                        , modeldef  :: TxsDefs.ModelDef
                        , mapperdef :: Maybe TxsDefs.MapperDef
                        , purpdef   :: Maybe TxsDefs.PurpDef
                        , puttow    :: TxsDDefs.Action -> IOC TxsDDefs.Action
                        , getfrow   :: IOC TxsDDefs.Action
                        , behtrie   :: [ (EnvData.StateNr, TxsDDefs.Action, EnvData.StateNr) ]
                                                                     -- behaviour trie
  initial beh statenr
  current beh statenr
                        , modsts    :: BTree.BTree                      -- model state
                        , mapsts    :: BTree.BTree                      -- mapper state
                        , purpsts   :: [(TxsDefs.GoalId,Either BTree.BTree TxsDDefs.PurpVerdict)]   -- purpose state
                        , putmsgs   :: [EnvData.Msg] -> IOC ()       -- (error) reporting
                        , chanoffers :: Map.Map (Name, Int) VarId.VarId    -- substitution for channel offers (LPE translation)
                        }
  named smt solver envs
  TorXakis definitions
  TorXakis signatures
                        , modeldef  :: TxsDefs.ModelDef
                        , mapperdef :: Maybe TxsDefs.MapperDef
                        , puttow    :: TxsDDefs.Action -> IOC TxsDDefs.Action
                        , getfrow   :: IOC TxsDDefs.Action
                        , behtrie   :: [(EnvData.StateNr,TxsDDefs.Action,EnvData.StateNr)]
                                                                     -- behaviour trie
  initial beh statenr
  current beh statenr
                        , modsts    :: BTree.BTree                   -- model state
                        , mapsts    :: BTree.BTree                   -- mapper state
                        , putmsgs   :: [EnvData.Msg] -> IOC ()       -- (error) reporting
                        , chanoffers :: Map.Map (Name, Int) VarId.VarId    -- substitution for channel offers (LPE translation)
                        }
  named smt solver envs
  TorXakis definitions
  TorXakis signatures
                        , modeldef  :: TxsDefs.ModelDef
                        , behtrie   :: [(EnvData.StateNr,TxsDDefs.Action,EnvData.StateNr)]
                                                                     -- behaviour trie
  initial beh statenr
  current beh statenr
  max beh statenr
                        , modstss   :: Map.Map EnvData.StateNr BTree.BTree   -- model state
                        , putmsgs   :: [EnvData.Msg] -> IOC ()       -- (error) reporting
                        , chanoffers :: Map.Map (Name, Int) VarId.VarId    -- substitution for channel offers (LPE translation)
                        }


modifyCS :: (CoreState -> CoreState) -> IOC ()
modifyCS f  = modify $ \env -> env { state = f (state env) }

putCS :: CoreState -> IOC ()
putCS newSt = modify $ \env -> env { state = newSt }

incUnid :: IOC ()
incUnid = modify $ \env -> env { unid = unid env + 1}

-- ----------------------------------------------------------------------------------------- --
  SMT :   getting and setting SMT solver

getSMT :: String -> IOC SMTData.SmtEnv
getSMT smtname = do
     smts'    <- gets (smts . state)
     putMsgs' <- gets (putmsgs . state)
     case Map.lookup smtname smts' of
       Nothing     -> if  not $ Map.null smts'
                        then do putMsgs' [ EnvData.TXS_CORE_SYSTEM_WARNING
                                          $ "No such Solver: " ++ smtname ]
                                let (name',smtenv) = head $ Map.toList smts'
                                putMsgs' [ EnvData.TXS_CORE_SYSTEM_WARNING
                                          $ "Using instead: " ++ name' ]
                                return smtenv
                        else do putMsgs' [ EnvData.TXS_CORE_SYSTEM_ERROR
                                          $ "No such Solver: " ++ smtname ]
                                return SMTData.SmtEnvError
       Just smtenv -> return smtenv

putSMT :: String -> SMTData.SmtEnv -> IOC ()
putSMT smtname smtenv = do
  st <- gets state
  let smts' = smts st
      state' = st { smts = Map.insert smtname smtenv smts'}
  modify $ \env -> env { state = state' }

-- ----------------------------------------------------------------------------------------- --
  Params :   getParams , 

getParams :: [String] -> IOC [(String,String)]
getParams prms =
     case prms of
       [] -> map (\(nm,(val,_))->(nm,val)) . Map.toList <$> gets params
       _  -> concat <$> mapM getParam prms

getParam :: String -> IOC [(String,String)]
getParam prm = do
     params' <- gets params
     case Map.lookup prm params' of
       Nothing           -> return []
       Just (val,_check) -> return [(prm,val)]

setParams :: [(String,String)] -> IOC [(String,String)]
setParams parvals = concat <$> mapM setParam parvals

setParam :: (String,String) -> IOC [(String,String)]
setParam (prm,val) = do
     params' <- gets params
     case Map.lookup prm params' of
       Nothing           -> return []
       Just (_,check)    -> if check val
                              then let newParams = Map.insert prm (val,check) params'
                                    in do
                                      modify $ \env -> env { params = newParams }
                                      return [(prm,val)]
                              else return []

-- ----------------------------------------------------------------------------------------- --
-- Unid :  unique (negative) number for identifiers

initUnid :: IOC Id
initUnid = return (-1)

newUnid :: IOC Id
newUnid = do
     uid <- gets unid
     modify $ \env -> env { unid = uid - 1 }
     return $ uid - 1

-- ----------------------------------------------------------------------------------------- --
-- put messages

putMsgs :: [EnvData.Msg] -> IOC ()
putMsgs msg = do
     putMsgs' <- gets (putmsgs . state)
     putMsgs' msg

putInfo :: [String] -> IOC ()
putInfo = mapM_ (\m -> putMsgs [ EnvData.TXS_CORE_USER_INFO m ])

-- ----------------------------------------------------------------------------------------- --
  set ChanOffers ( needed during LPE translation )

setChanoffers :: Map.Map (Name, Int) VarId.VarId -> IOC ()
setChanoffers mapping = do 
    st <- gets state  
    let state' = st { chanoffers = mapping }
    modify $ \env -> env { state = state' }

getChanoffers :: IOC (Map.Map (Name, Int) VarId.VarId)
getChanoffers = gets (chanoffers . state)
-- ----------------------------------------------------------------------------------------- --
--
-- ----------------------------------------------------------------------------------------- --

 torxakis core main state monad transformer
 :: [String] -> IOC [(String,String)]
 :: [(String,String)] -> IOC [(String,String)]
 :: IOC.IOC Int
 :: IOC.IOC Int
 :: [EnvData.Msg] -> IOC ()
 :: [String] -> IOC ()
 * Operation on core-state
 import from local
 import from solve
 ----------------------------------------------------------------------------------------- --
 ^ Core configuration.
 ^ Last used unique number.
 ^ State specific information.
 (error) reporting
 substitution for channel offers (LPE translation)
 behaviour trie
 model state
 mapper state
 purpose state
 (error) reporting
 substitution for channel offers (LPE translation)
 behaviour trie
 model state
 mapper state
 (error) reporting
 substitution for channel offers (LPE translation)
 behaviour trie
 model state
 (error) reporting
 substitution for channel offers (LPE translation)
 ----------------------------------------------------------------------------------------- --
 ----------------------------------------------------------------------------------------- --
 ----------------------------------------------------------------------------------------- --
 Unid :  unique (negative) number for identifiers
 ----------------------------------------------------------------------------------------- --
 put messages
 ----------------------------------------------------------------------------------------- --
 ----------------------------------------------------------------------------------------- --

 ----------------------------------------------------------------------------------------- --

 TorXakis - Model Based Testing 
 Copyright ( c ) 2015 - 2017 TNO and Radboud University 
 See LICENSE at root directory of this repository . 

TorXakis - Model Based Testing
Copyright (c) 2015-2017 TNO and Radboud University
See LICENSE at root directory of this repository.
-}


# LANGUAGE FlexibleInstances #
  | TorXakis Core Environment ( Internal State ) Data Type Definitions .
module EnvCore
  IOC = StateT EnvC IO
  , EnvC(..)
  , CoreState(..)
  : : String - > IOC SMTData . SmtEnv
  : : String - > SMTData . SmtEnv - > IOC ( )
  , modifyCS
  , putCS
  , incUnid
  )
where

import           Control.Monad.State hiding (state)

import qualified Data.Map            as Map


import           Config    hiding (setParams)
import qualified EnvBasic    as EnvB
import qualified EnvData
import qualified ParamCore

  import from behavedefs
import qualified BTree

  import from defs
import qualified Sigs
import qualified TxsDDefs
import qualified TxsDefs

  import from valexpr
import           Id
import qualified VarId               (VarId)
import           Name

import qualified SMTData

  IOC :   torxakis core state monad transformer

type  IOC  = StateT EnvC IO

   ( StateT IOC.EnvC IO )
  where
     newUnid  =  newUnid
     putMsgs  =  putMsgs
     setChanoffers = setChanoffers
     getChanoffers = getChanoffers
 

data EnvC = EnvC
  , params :: ParamCore.Params
  }

data CoreState = Noning
  named smt solver envs
  TorXakis definitions
  TorXakis signatures
                        }
  named smt solver envs
  TorXakis definitions
  TorXakis signatures
                        , modeldef  :: TxsDefs.ModelDef
                        , mapperdef :: Maybe TxsDefs.MapperDef
                        , purpdef   :: Maybe TxsDefs.PurpDef
                        , puttow    :: TxsDDefs.Action -> IOC TxsDDefs.Action
                        , getfrow   :: IOC TxsDDefs.Action
                        , behtrie   :: [ (EnvData.StateNr, TxsDDefs.Action, EnvData.StateNr) ]
  initial beh statenr
  current beh statenr
                        }
  named smt solver envs
  TorXakis definitions
  TorXakis signatures
                        , modeldef  :: TxsDefs.ModelDef
                        , mapperdef :: Maybe TxsDefs.MapperDef
                        , puttow    :: TxsDDefs.Action -> IOC TxsDDefs.Action
                        , getfrow   :: IOC TxsDDefs.Action
                        , behtrie   :: [(EnvData.StateNr,TxsDDefs.Action,EnvData.StateNr)]
  initial beh statenr
  current beh statenr
                        }
  named smt solver envs
  TorXakis definitions
  TorXakis signatures
                        , modeldef  :: TxsDefs.ModelDef
                        , behtrie   :: [(EnvData.StateNr,TxsDDefs.Action,EnvData.StateNr)]
  initial beh statenr
  current beh statenr
  max beh statenr
                        }


modifyCS :: (CoreState -> CoreState) -> IOC ()
modifyCS f  = modify $ \env -> env { state = f (state env) }

putCS :: CoreState -> IOC ()
putCS newSt = modify $ \env -> env { state = newSt }

incUnid :: IOC ()
incUnid = modify $ \env -> env { unid = unid env + 1}

  SMT :   getting and setting SMT solver

getSMT :: String -> IOC SMTData.SmtEnv
getSMT smtname = do
     smts'    <- gets (smts . state)
     putMsgs' <- gets (putmsgs . state)
     case Map.lookup smtname smts' of
       Nothing     -> if  not $ Map.null smts'
                        then do putMsgs' [ EnvData.TXS_CORE_SYSTEM_WARNING
                                          $ "No such Solver: " ++ smtname ]
                                let (name',smtenv) = head $ Map.toList smts'
                                putMsgs' [ EnvData.TXS_CORE_SYSTEM_WARNING
                                          $ "Using instead: " ++ name' ]
                                return smtenv
                        else do putMsgs' [ EnvData.TXS_CORE_SYSTEM_ERROR
                                          $ "No such Solver: " ++ smtname ]
                                return SMTData.SmtEnvError
       Just smtenv -> return smtenv

putSMT :: String -> SMTData.SmtEnv -> IOC ()
putSMT smtname smtenv = do
  st <- gets state
  let smts' = smts st
      state' = st { smts = Map.insert smtname smtenv smts'}
  modify $ \env -> env { state = state' }

  Params :   getParams , 

getParams :: [String] -> IOC [(String,String)]
getParams prms =
     case prms of
       [] -> map (\(nm,(val,_))->(nm,val)) . Map.toList <$> gets params
       _  -> concat <$> mapM getParam prms

getParam :: String -> IOC [(String,String)]
getParam prm = do
     params' <- gets params
     case Map.lookup prm params' of
       Nothing           -> return []
       Just (val,_check) -> return [(prm,val)]

setParams :: [(String,String)] -> IOC [(String,String)]
setParams parvals = concat <$> mapM setParam parvals

setParam :: (String,String) -> IOC [(String,String)]
setParam (prm,val) = do
     params' <- gets params
     case Map.lookup prm params' of
       Nothing           -> return []
       Just (_,check)    -> if check val
                              then let newParams = Map.insert prm (val,check) params'
                                    in do
                                      modify $ \env -> env { params = newParams }
                                      return [(prm,val)]
                              else return []


initUnid :: IOC Id
initUnid = return (-1)

newUnid :: IOC Id
newUnid = do
     uid <- gets unid
     modify $ \env -> env { unid = uid - 1 }
     return $ uid - 1


putMsgs :: [EnvData.Msg] -> IOC ()
putMsgs msg = do
     putMsgs' <- gets (putmsgs . state)
     putMsgs' msg

putInfo :: [String] -> IOC ()
putInfo = mapM_ (\m -> putMsgs [ EnvData.TXS_CORE_USER_INFO m ])

  set ChanOffers ( needed during LPE translation )

setChanoffers :: Map.Map (Name, Int) VarId.VarId -> IOC ()
setChanoffers mapping = do 
    st <- gets state  
    let state' = st { chanoffers = mapping }
    modify $ \env -> env { state = state' }

getChanoffers :: IOC (Map.Map (Name, Int) VarId.VarId)
getChanoffers = gets (chanoffers . state)
