content: {-
  Copyright (c) 2014-2015, Johan Nordlander, Jonas Duregård, Michał Pałka,
                           Patrik Jansson and Josef Svenningsson
  All rights reserved.
  
  Redistribution and use in source and binary forms, with or without
  modification, are permitted provided that the following conditions are met:
  
     * Redistributions of source code must retain the above copyright notice,
       this list of conditions and the following disclaimer.
     * Redistributions in binary form must reproduce the above copyright
       notice, this list of conditions and the following disclaimer in the
       documentation and/or other materials provided with the distribution.
     * Neither the name of the Chalmers University of Technology nor the names of its 
       contributors may be used to endorse or promote products derived from this 
       software without specific prior written permission.
  
  THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
  AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
  IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE
  DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE
  FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL
  DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR
  SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
  CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY,
  OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
  OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
  -}
  
  {-# LANGUAGE FlexibleInstances #-}
  module AR where
  import qualified Data.Map as Map
  import Data.Map (Map, keys, elems)
  import Data.List
  import Data.Maybe
  
  dom :: Map a b -> [a]
  rng :: Map a b -> [b]
  dom = keys
  rng = elems
  
  a `subsetof` b      = all (`elem` b) a
  a `equal` b         = a `subsetof` b && b `subsetof` a
  
  unique xs           = xs == nub xs
  
  data Component =
        Atomic      (Map PortName Port) (Map VarName Type)       [Runnable]
      | Composition (Map PortName Port) (Map CompName Component) [Connector]
  
  ports (Atomic iface _ _)        = iface
  ports (Composition iface _ _)   = iface
  
  data PortKind =
        SenderReceiver (Map VarName Type)   
      | ClientServer   (Map OpName Operation)  -- a sum (choice) of operations
      
  instance Eq PortKind where
      SenderReceiver ts == SenderReceiver ts'  =  ts == ts'
      ClientServer ops  == ClientServer ops'   =  ops == ops'
      _ == _          = False
  
  data Port = Provided PortKind
            | Required PortKind
      deriving Eq
  
  inverse (Provided p)    = Required p
  inverse (Required p)    = Provided p
  
  data Operation =
      Op (Map VarName ArgType) [Int]  -- ^ a product (tuple) of arguments, set of error codes
  
  instance Eq Operation where
      Op args errs == Op args' errs'  = args == args' && errs == errs'
      
  data ArgType   = 
      In    Type
    | InOut Type
    | Out   Type
      deriving Eq
  
  type Connector  = (PortRef, PortRef)    
  
  data PortRef = 
      Qual CompName PortName
    | Ext PortName
      deriving Eq
  
  type PortName   = String
  type CompName   = String
  type FieldName  = String
  type TagName    = String
  type OpName     = String
  type VarName    = String
  
  type Statevars  = Map VarName Value
  type Arguments  = Map VarName Value
  type Response   = Either Int (Map VarName Value)
  
  -- | Four different kinds of |Runnable|s
  data Runnable = 
      Init Behavior    -- ^ should set up initial state etc.
    | DataReceived     PortName         (Statevars -> Arguments -> Behavior)
      -- ^ async. method
    | OperationInvoked PortName OpName  (Statevars -> Arguments -> Behavior)
      -- ^ sync. operation
    | Timing           Double           (Statevars -> Behavior)
      -- ^ repeated execution
  
  {- There are different classes of runnables. This type is not covering
  all of them. For example, in the full AUTOSAR standard, a runnable
  could have a set of waitPoints, but this simplified description
  assumes this set is empty.  -}
  
  
  -- | Observable effect of a |Runnable|
  data Behavior = 
      Sending   PortName Arguments Behavior 
      -- ^ 
    | Invoking  PortName OpName Arguments (Response -> Behavior) 
      -- ^ Invoke operation (must check "port matching")
    | Responding Response Behavior
      -- ^ Act. on a call (might be better to merge with Idling)
    | Idling Statevars
    | Crashed
    | Comp (Map CompName Behavior)
  
  data Observation =
      Send    PortRef Arguments
    | Invoke  PortRef OpName Arguments
    | Respond Response
    | Tau
  
  update :: k -> v -> Map k v -> Map k v
  update       = undefined
  
  connections :: env -> CompName -> PortName -> [PortRef]
  connections  = undefined
  
  runnables :: env -> CompName -> [Runnable]
  runnables    = undefined
  
  data Msg = Msg CompName PortName Arguments deriving Eq
  
  type ComponentLinks = [(CompName, CompName)]
  
  -- | perhaps a queue or at least timestamped messages
  type MsgPool = [Msg] 
  
  type State = (Map CompName Behavior, MsgPool, ComponentLinks)
  
  reduce :: env -> State -> [(State, Observation)]
  reduce env (bhvs, msgs, links) = 
  
      [ ((update c next bhvs, Msg c' p' args : msgs, links), Tau)
      | (c,Sending p args next) <- Map.assocs bhvs
      , Qual c' p' <- connections env c p
      ] ++
      
      [ ((update c (run svars args) bhvs, delete (Msg c p args) msgs, links), Tau) 
      | (c,Idling svars) <- Map.assocs bhvs
      , DataReceived p run <- runnables env c
      , Msg c1 p1 args <- msgs
      , c == c1, p == p1
      ] ++
      
      [ ((update c' (run svars args) bhvs, msgs, (c,c'):links), Tau) 
      | (c,Invoking p op args cont) <- Map.assocs bhvs
      , (c',Idling svars) <- Map.assocs bhvs
      , OperationInvoked p' op' run <- runnables env c'
      , Qual c' p' `elem` connections env c p
      ] ++
      
      [ ((update c (cont resp) (update c' next bhvs), msgs, delete (c,c') links), Tau) 
      | (c,Invoking p op args cont) <- Map.assocs bhvs
      , (c',Responding resp next) <- Map.assocs bhvs
      , (c,c') `elem` links
      ] ++
      
      [ ((update c next bhvs, msgs, links), Send (Ext p') args) 
      | (c,Sending p args next) <- Map.assocs bhvs
      , Ext p' <- connections env c p
      ] ++
  
      [ ((update c (Invoking p op args cont) bhvs, msgs, links), Invoke (Ext p') op args) 
      | (c,Invoking p op args cont) <- Map.assocs bhvs
      , Ext p' <- connections env c p
      ] ++
  
      [ ]
  
  --------------------------------------------------------------
              
  validComp partial (Atomic iface sig runns)
                              = unique (dom iface) &&
                                unique int_rcvs && 
                                unique int_ops &&
                                int_rcvs `subsetof` ext_rcvs && int_ops `subsetof` ext_ops &&
                                (partial || total)
    where ext_rcvs            = [ p | (p, Provided (SenderReceiver _)) <- Map.assocs iface ]
          ext_ops             = [ (p,o) | (p, Provided (ClientServer ops)) <- Map.assocs iface, o <- dom ops ]
          int_rcvs            = [ p | DataReceived p _ <- runns ]
          int_ops             = [ (p,o) | OperationInvoked p o _ <- runns ]
          total               = ext_rcvs `subsetof` int_rcvs && ext_ops `subsetof` int_ops
  validComp partial (Composition iface comps conns)
                              = unique (dom iface) &&
                                unique (dom comps) && 
                                all (validComp partial) (rng comps) &&
                                all (validConn all_ports) conns &&
                                all (== 1) (map fan_out req_clisrv) &&
                                all (>= 1) (map fan_out req_sndrcv)
    where all_ports           = [ (Qual c p, port) 
                                | (c,comp) <- Map.assocs comps, (p,port) <- Map.assocs $ ports comp ] ++
                                [ (Ext p, inverse port) 
                                | (p,port) <- Map.assocs iface ]
          req_sndrcv          = [ r | (r,Required (SenderReceiver _)) <- all_ports ]
          req_clisrv          = [ r | (r,Required (ClientServer _)) <- all_ports ]
          fan_out r           = length [ q | (p,q) <- conns, p == r ]
  
  validConn ports (r,r')      = case (lookup r ports, lookup r' ports) of
                                  (Just (Required p), Just (Provided p')) -> p == p'
                                  _ -> False
  
  
  ------------------------------------------------------------------
  
  data Type =
      TInt                            
    | TBool                           
    | TChar                           
    | TArray  Type                    
    | TStruct (Map FieldName Type)    
    | TUnion  (Map TagName Type)
  
  instance Eq Type where
      TInt == TInt                    = True
      TBool == TBool                  = True
      TChar == TChar                  = True
      TArray t == TArray t'           = t == t'
      TStruct ts == TStruct ts'       = ts == ts'
      TUnion ts == TUnion ts'         = ts == ts'
      _ == _                          = False
  
  data Value =
      VInt Int                        
    | VBool Bool                      
    | VChar Char                      
    | VArray [Value]                  
    | VStruct (Map FieldName Value)   
    | VUnion TagName Value
      deriving Eq
  
  hasType TInt           (VInt _)        = True
  hasType TBool          (VBool _)       = True
  hasType TChar          (VChar _)       = True
  hasType (TArray t)     (VArray vs)     = all (hasType t) vs
  hasType (TStruct ts)   (VStruct fs)    = unique (dom fs) && dom ts `equal` dom fs &&
                                           and [ hasTypeIn ts f v | (f,v) <- Map.assocs fs ]
  hasType (TUnion ts)    (VUnion tag v)  = hasTypeIn ts tag v
  
  hasTypeIn ts k v = case Map.lookup k ts of 
                       Just t  -> hasType t v; 
                       _       -> False
  
  