    {-# LANGUAGE ExistentialQuantification #-}
    {-# LANGUAGE GADTs                     #-}
    {-# LANGUAGE RankNTypes                #-}
    {-# LANGUAGE Safe                      #-}

    -- | Specification of Copilot streams as modular transition systems.
    module Copilot.Theorem.TransSys.Spec
      ( module Copilot.Theorem.TransSys.Operators
      , module Copilot.Theorem.TransSys.Type
      , module Copilot.Theorem.TransSys.Invariants
      , TransSys (..)
      , Node (..)
      , PropId
      , NodeId
      , Var (..)
      , ExtVar (..)
      , VarDef (..)
      , VarDescr (..)
      , Expr (..)
      , mkExtVar
      , transformExpr
      , isTopologicallySorted
      , nodeVarsSet
      , specDependenciesGraph
      , specTopNode ) where

    import qualified Copilot.Core as C

    import Copilot.Theorem.TransSys.Type
    import Copilot.Theorem.TransSys.Operators
    import Copilot.Theorem.TransSys.Invariants

    import Copilot.Theorem.Misc.Utils

    import Control.Applicative (liftA2)
    import Control.Monad (foldM, guard)

    import Data.Maybe
    import Data.Monoid ((<>))
    import Data.Map (Map)
    import Data.Set (Set, isSubsetOf, member)
    import Data.Bimap (Bimap)

    import qualified Data.List  as List
    import qualified Data.Map   as Map
    import qualified Data.Set   as Set
    import qualified Data.Bimap as Bimap

    -- | Unique name that identifies a node.
    type NodeId = String

    -- | Unique name that identifies a property.
    type PropId = String

    -- | A modular transition system is defined by a graph of nodes and a series
    -- of properties, each mapped to a variable and a 'C.Prop' describing how the
    -- property is quantified.
    data TransSys = TransSys
      { TransSys -> [Node]
    specNodes         :: [Node]
      , TransSys -> NodeId
    specTopNodeId     :: NodeId
      , TransSys -> Map NodeId (ExtVar, Prop)
    specProps         :: Map PropId (ExtVar, C.Prop) }

    -- | A node is a set of variables living in a local namespace and corresponding
    -- to the 'Var' type.
    data Node = Node
      { Node -> NodeId
    nodeId            :: NodeId
      , Node -> [NodeId]
    nodeDependencies  :: [NodeId]          -- ^ Nodes from which variables are
                                               --   imported.
      , Node -> Map Var VarDescr
    nodeLocalVars     :: Map Var VarDescr  -- ^ Locally defined variables,
                                               --   either as the previous value of
                                               --   another variable (using 'Pre'),
                                               --   an expression involving
                                               --   variables (using 'Expr') or a
                                               --   set of constraints (using
                                               --   'Constrs').
      , Node -> Bimap Var ExtVar
    nodeImportedVars  :: Bimap Var ExtVar  -- ^ Binds each imported variable to
                                               --   its local name.
      , Node -> [Expr Bool]
    nodeConstrs       :: [Expr Bool] }

    -- | Identifer of a variable in the local (within one node) namespace.
    data Var      =  Var {Var -> NodeId
    varName :: String}
      deriving (Var -> Var -> Bool
    (Var -> Var -> Bool) -> (Var -> Var -> Bool) -> Eq Var
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    $c== :: Var -> Var -> Bool
    == :: Var -> Var -> Bool
    $c/= :: Var -> Var -> Bool
    /= :: Var -> Var -> Bool
    Eq, Int -> Var -> ShowS
    [Var] -> ShowS
    Var -> NodeId
    (Int -> Var -> ShowS)
    -> (Var -> NodeId) -> ([Var] -> ShowS) -> Show Var
    forall a.
    (Int -> a -> ShowS) -> (a -> NodeId) -> ([a] -> ShowS) -> Show a
    $cshowsPrec :: Int -> Var -> ShowS
    showsPrec :: Int -> Var -> ShowS
    $cshow :: Var -> NodeId
    show :: Var -> NodeId
    $cshowList :: [Var] -> ShowS
    showList :: [Var] -> ShowS
    Show, Eq Var
    Eq Var =>
    (Var -> Var -> Ordering)
    -> (Var -> Var -> Bool)
    -> (Var -> Var -> Bool)
    -> (Var -> Var -> Bool)
    -> (Var -> Var -> Bool)
    -> (Var -> Var -> Var)
    -> (Var -> Var -> Var)
    -> Ord Var
    Var -> Var -> Bool
    Var -> Var -> Ordering
    Var -> Var -> Var
    forall a.
    Eq a =>
    (a -> a -> Ordering)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> a)
    -> (a -> a -> a)
    -> Ord a
    $ccompare :: Var -> Var -> Ordering
    compare :: Var -> Var -> Ordering
    $c< :: Var -> Var -> Bool
    < :: Var -> Var -> Bool
    $c<= :: Var -> Var -> Bool
    <= :: Var -> Var -> Bool
    $c> :: Var -> Var -> Bool
    > :: Var -> Var -> Bool
    $c>= :: Var -> Var -> Bool
    >= :: Var -> Var -> Bool
    $cmax :: Var -> Var -> Var
    max :: Var -> Var -> Var
    $cmin :: Var -> Var -> Var
    min :: Var -> Var -> Var
    Ord)

    -- | Identifer of a variable in the global namespace by specifying both a node
    -- name and a variable.
    data ExtVar   =  ExtVar {ExtVar -> NodeId
    extVarNode :: NodeId, ExtVar -> Var
    extVarLocalPart :: Var }
      deriving (ExtVar -> ExtVar -> Bool
    (ExtVar -> ExtVar -> Bool)
    -> (ExtVar -> ExtVar -> Bool) -> Eq ExtVar
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    $c== :: ExtVar -> ExtVar -> Bool
    == :: ExtVar -> ExtVar -> Bool
    $c/= :: ExtVar -> ExtVar -> Bool
    /= :: ExtVar -> ExtVar -> Bool
    Eq, Eq ExtVar
    Eq ExtVar =>
    (ExtVar -> ExtVar -> Ordering)
    -> (ExtVar -> ExtVar -> Bool)
    -> (ExtVar -> ExtVar -> Bool)
    -> (ExtVar -> ExtVar -> Bool)
    -> (ExtVar -> ExtVar -> Bool)
    -> (ExtVar -> ExtVar -> ExtVar)
    -> (ExtVar -> ExtVar -> ExtVar)
    -> Ord ExtVar
    ExtVar -> ExtVar -> Bool
    ExtVar -> ExtVar -> Ordering
    ExtVar -> ExtVar -> ExtVar
    forall a.
    Eq a =>
    (a -> a -> Ordering)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> a)
    -> (a -> a -> a)
    -> Ord a
    $ccompare :: ExtVar -> ExtVar -> Ordering
    compare :: ExtVar -> ExtVar -> Ordering
    $c< :: ExtVar -> ExtVar -> Bool
    < :: ExtVar -> ExtVar -> Bool
    $c<= :: ExtVar -> ExtVar -> Bool
    <= :: ExtVar -> ExtVar -> Bool
    $c> :: ExtVar -> ExtVar -> Bool
    > :: ExtVar -> ExtVar -> Bool
    $c>= :: ExtVar -> ExtVar -> Bool
    >= :: ExtVar -> ExtVar -> Bool
    $cmax :: ExtVar -> ExtVar -> ExtVar
    max :: ExtVar -> ExtVar -> ExtVar
    $cmin :: ExtVar -> ExtVar -> ExtVar
    min :: ExtVar -> ExtVar -> ExtVar
    Ord)

    -- | A description of a variable together with its type.
    data VarDescr = forall t . VarDescr
      { ()
    varType :: Type t
      , ()
    varDef  :: VarDef t }

    -- | A variable definition either as a delay, an operation on variables, or
    -- a constraint.
    data VarDef t = Pre t Var | Expr (Expr t) | Constrs [Expr Bool]

    -- | A point-wise (time-wise) expression.
    data Expr t where
      Const :: Type t -> t -> Expr t
      Ite   :: Type t -> Expr Bool -> Expr t -> Expr t -> Expr t
      Op1   :: Type t -> Op1 t -> Expr t -> Expr t
      Op2   :: Type t -> Op2 a t -> Expr a -> Expr a -> Expr t
      VarE  :: Type t -> Var -> Expr t

    -- | Constructor for variables identifiers in the global namespace.
    mkExtVar :: NodeId -> NodeId -> ExtVar
    mkExtVar NodeId
    node NodeId
    name = NodeId -> Var -> ExtVar
    ExtVar NodeId
    node (NodeId -> Var
    Var NodeId
    name)

    foldExpr :: (Monoid m) => (forall t . Expr t -> m) -> Expr a -> m
    foldExpr :: forall m a. Monoid m => (forall t. Expr t -> m) -> Expr a -> m
    foldExpr forall t. Expr t -> m
    f Expr a
    expr = Expr a -> m
    forall t. Expr t -> m
    f Expr a
    expr m -> m -> m
    forall a. Semigroup a => a -> a -> a
    <> m
    fargs
      where
        fargs :: m
    fargs = case Expr a
    expr of
          (Ite Type a
    _ Expr Bool
    c Expr a
    e1 Expr a
    e2)  -> (forall t. Expr t -> m) -> Expr Bool -> m
    forall m a. Monoid m => (forall t. Expr t -> m) -> Expr a -> m
    foldExpr Expr t -> m
    forall t. Expr t -> m
    f Expr Bool
    c m -> m -> m
    forall a. Semigroup a => a -> a -> a
    <> (forall t. Expr t -> m) -> Expr a -> m
    forall m a. Monoid m => (forall t. Expr t -> m) -> Expr a -> m
    foldExpr Expr t -> m
    forall t. Expr t -> m
    f Expr a
    e1 m -> m -> m
    forall a. Semigroup a => a -> a -> a
    <> (forall t. Expr t -> m) -> Expr a -> m
    forall m a. Monoid m => (forall t. Expr t -> m) -> Expr a -> m
    foldExpr Expr t -> m
    forall t. Expr t -> m
    f Expr a
    e2
          (Op1 Type a
    _ Op1 a
    _ Expr a
    e)      -> (forall t. Expr t -> m) -> Expr a -> m
    forall m a. Monoid m => (forall t. Expr t -> m) -> Expr a -> m
    foldExpr Expr t -> m
    forall t. Expr t -> m
    f Expr a
    e
          (Op2 Type a
    _ Op2 a a
    _ Expr a
    e1 Expr a
    e2)  -> (forall t. Expr t -> m) -> Expr a -> m
    forall m a. Monoid m => (forall t. Expr t -> m) -> Expr a -> m
    foldExpr Expr t -> m
    forall t. Expr t -> m
    f Expr a
    e1 m -> m -> m
    forall a. Semigroup a => a -> a -> a
    <> (forall t. Expr t -> m) -> Expr a -> m
    forall m a. Monoid m => (forall t. Expr t -> m) -> Expr a -> m
    foldExpr Expr t -> m
    forall t. Expr t -> m
    f Expr a
    e2
          Expr a
    _                -> m
    forall a. Monoid a => a
    mempty

    foldUExpr :: (Monoid m) => (forall t . Expr t -> m) -> U Expr -> m
    foldUExpr :: forall m. Monoid m => (forall t. Expr t -> m) -> U Expr -> m
    foldUExpr forall t. Expr t -> m
    f (U Expr t
    e) = (forall t. Expr t -> m) -> Expr t -> m
    forall m a. Monoid m => (forall t. Expr t -> m) -> Expr a -> m
    foldExpr Expr t -> m
    forall t. Expr t -> m
    f Expr t
    e

    -- | Apply an arbitrary transformation to the leafs of an expression.
    transformExpr :: (forall a . Expr a -> Expr a) -> Expr t -> Expr t
    transformExpr :: forall t. (forall a. Expr a -> Expr a) -> Expr t -> Expr t
    transformExpr forall a. Expr a -> Expr a
    f = Expr t -> Expr t
    forall a. Expr a -> Expr a
    tre
      where
        tre :: forall t . Expr t -> Expr t
        tre :: forall a. Expr a -> Expr a
    tre (Ite Type t
    t Expr Bool
    c Expr t
    e1 Expr t
    e2)   = Expr t -> Expr t
    forall a. Expr a -> Expr a
    f (Type t -> Expr Bool -> Expr t -> Expr t -> Expr t
    forall t. Type t -> Expr Bool -> Expr t -> Expr t -> Expr t
    Ite Type t
    t (Expr Bool -> Expr Bool
    forall a. Expr a -> Expr a
    tre Expr Bool
    c) (Expr t -> Expr t
    forall a. Expr a -> Expr a
    tre Expr t
    e1) (Expr t -> Expr t
    forall a. Expr a -> Expr a
    tre Expr t
    e2))
        tre (Op1 Type t
    t Op1 t
    op Expr t
    e)      = Expr t -> Expr t
    forall a. Expr a -> Expr a
    f (Type t -> Op1 t -> Expr t -> Expr t
    forall t. Type t -> Op1 t -> Expr t -> Expr t
    Op1 Type t
    t Op1 t
    op (Expr t -> Expr t
    forall a. Expr a -> Expr a
    tre Expr t
    e))
        tre (Op2 Type t
    t Op2 a t
    op Expr a
    e1 Expr a
    e2)  = Expr t -> Expr t
    forall a. Expr a -> Expr a
    f (Type t -> Op2 a t -> Expr a -> Expr a -> Expr t
    forall t a. Type t -> Op2 a t -> Expr a -> Expr a -> Expr t
    Op2 Type t
    t Op2 a t
    op (Expr a -> Expr a
    forall a. Expr a -> Expr a
    tre Expr a
    e1) (Expr a -> Expr a
    forall a. Expr a -> Expr a
    tre Expr a
    e2))
        tre Expr t
    e                 = Expr t -> Expr t
    forall a. Expr a -> Expr a
    f Expr t
    e

    -- | The set of variables related to a node (union of the local variables and
    -- the imported variables after deferencing them).
    nodeVarsSet :: Node -> Set Var
    nodeVarsSet :: Node -> Set Var
    nodeVarsSet = (Set Var -> Set Var -> Set Var)
    -> (Node -> Set Var) -> (Node -> Set Var) -> Node -> Set Var
    forall a b c.
    (a -> b -> c) -> (Node -> a) -> (Node -> b) -> Node -> c
    forall (f :: * -> *) a b c.
    Applicative f =>
    (a -> b -> c) -> f a -> f b -> f c
    liftA2 Set Var -> Set Var -> Set Var
    forall a. Ord a => Set a -> Set a -> Set a
    Set.union
      Node -> Set Var
    nodeLocalVarsSet
      (Map Var ExtVar -> Set Var
    forall k a. Map k a -> Set k
    Map.keysSet (Map Var ExtVar -> Set Var)
    -> (Node -> Map Var ExtVar) -> Node -> Set Var
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Bimap Var ExtVar -> Map Var ExtVar
    forall a b. Bimap a b -> Map a b
    Bimap.toMap  (Bimap Var ExtVar -> Map Var ExtVar)
    -> (Node -> Bimap Var ExtVar) -> Node -> Map Var ExtVar
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Node -> Bimap Var ExtVar
    nodeImportedVars)

    nodeLocalVarsSet :: Node -> Set Var
    nodeLocalVarsSet :: Node -> Set Var
    nodeLocalVarsSet = Map Var VarDescr -> Set Var
    forall k a. Map k a -> Set k
    Map.keysSet (Map Var VarDescr -> Set Var)
    -> (Node -> Map Var VarDescr) -> Node -> Set Var
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Node -> Map Var VarDescr
    nodeLocalVars

    nodeRhsVarsSet :: Node -> Set Var
    nodeRhsVarsSet :: Node -> Set Var
    nodeRhsVarsSet Node
    n =
      let varOcc :: Expr t -> Set Var
    varOcc (VarE Type t
    _ Var
    v) = Var -> Set Var
    forall a. a -> Set a
    Set.singleton Var
    v
          varOcc Expr t
    _          = Set Var
    forall a. Set a
    Set.empty

          descrRhsVars :: VarDescr -> Set Var
    descrRhsVars (VarDescr Type t
    _ (Expr Expr t
    e))      = (forall t. Expr t -> Set Var) -> Expr t -> Set Var
    forall m a. Monoid m => (forall t. Expr t -> m) -> Expr a -> m
    foldExpr Expr t -> Set Var
    forall t. Expr t -> Set Var
    varOcc Expr t
    e
          descrRhsVars (VarDescr Type t
    _ (Pre t
    _ Var
    v))     = Var -> Set Var
    forall a. a -> Set a
    Set.singleton Var
    v
          descrRhsVars (VarDescr Type t
    _ (Constrs [Expr Bool]
    cs))  =
            [Set Var] -> Set Var
    forall a. Monoid a => [a] -> a
    mconcat ((Expr Bool -> Set Var) -> [Expr Bool] -> [Set Var]
    forall a b. (a -> b) -> [a] -> [b]
    map ((forall t. Expr t -> Set Var) -> Expr Bool -> Set Var
    forall m a. Monoid m => (forall t. Expr t -> m) -> Expr a -> m
    foldExpr Expr t -> Set Var
    forall t. Expr t -> Set Var
    varOcc) [Expr Bool]
    cs)

      in (VarDescr -> Set Var -> Set Var)
    -> Set Var -> Map Var VarDescr -> Set Var
    forall a b k. (a -> b -> b) -> b -> Map k a -> b
    Map.foldr (Set Var -> Set Var -> Set Var
    forall a. Ord a => Set a -> Set a -> Set a
    Set.union (Set Var -> Set Var -> Set Var)
    -> (VarDescr -> Set Var) -> VarDescr -> Set Var -> Set Var
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . VarDescr -> Set Var
    descrRhsVars) Set Var
    forall a. Set a
    Set.empty (Node -> Map Var VarDescr
    nodeLocalVars Node
    n)

    nodeImportedExtVarsSet :: Node -> Set ExtVar
    nodeImportedExtVarsSet :: Node -> Set ExtVar
    nodeImportedExtVarsSet = Map ExtVar Var -> Set ExtVar
    forall k a. Map k a -> Set k
    Map.keysSet (Map ExtVar Var -> Set ExtVar)
    -> (Node -> Map ExtVar Var) -> Node -> Set ExtVar
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Bimap Var ExtVar -> Map ExtVar Var
    forall a b. Bimap a b -> Map b a
    Bimap.toMapR (Bimap Var ExtVar -> Map ExtVar Var)
    -> (Node -> Bimap Var ExtVar) -> Node -> Map ExtVar Var
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Node -> Bimap Var ExtVar
    nodeImportedVars

    nodeExportedExtVarsSet :: Node -> Set ExtVar
    nodeExportedExtVarsSet :: Node -> Set ExtVar
    nodeExportedExtVarsSet Node
    n = (Var -> ExtVar) -> Set Var -> Set ExtVar
    forall b a. Ord b => (a -> b) -> Set a -> Set b
    Set.map (NodeId -> Var -> ExtVar
    ExtVar (NodeId -> Var -> ExtVar) -> NodeId -> Var -> ExtVar
    forall a b. (a -> b) -> a -> b
    $ Node -> NodeId
    nodeId Node
    n) (Node -> Set Var
    nodeLocalVarsSet Node
    n)

    instance HasInvariants Node where

      invariants :: Node -> [(NodeId, Bool)]
    invariants Node
    n =
        [ NodeId -> Bool -> (NodeId, Bool)
    prop NodeId
    "The dependencies declaration doesn't lie" (Bool -> (NodeId, Bool)) -> Bool -> (NodeId, Bool)
    forall a b. (a -> b) -> a -> b
    $
          ((ExtVar -> NodeId) -> [ExtVar] -> [NodeId]
    forall a b. (a -> b) -> [a] -> [b]
    map ExtVar -> NodeId
    extVarNode ([ExtVar] -> [NodeId])
    -> (Bimap Var ExtVar -> [ExtVar]) -> Bimap Var ExtVar -> [NodeId]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Bimap Var ExtVar -> [ExtVar]
    forall a b. Bimap a b -> [b]
    Bimap.elems (Bimap Var ExtVar -> [NodeId]) -> Bimap Var ExtVar -> [NodeId]
    forall a b. (a -> b) -> a -> b
    $ Node -> Bimap Var ExtVar
    nodeImportedVars Node
    n)
          [NodeId] -> [NodeId] -> Bool
    forall a. Ord a => [a] -> [a] -> Bool
    `isSublistOf` Node -> [NodeId]
    nodeDependencies Node
    n

        , NodeId -> Bool -> (NodeId, Bool)
    prop NodeId
    "All local variables are declared" (Bool -> (NodeId, Bool)) -> Bool -> (NodeId, Bool)
    forall a b. (a -> b) -> a -> b
    $
          Node -> Set Var
    nodeRhsVarsSet Node
    n Set Var -> Set Var -> Bool
    forall a. Ord a => Set a -> Set a -> Bool
    `isSubsetOf` Node -> Set Var
    nodeVarsSet Node
    n

        , NodeId -> Bool -> (NodeId, Bool)
    prop NodeId
    "Never apply 'pre' to an imported var" (Bool -> (NodeId, Bool)) -> Bool -> (NodeId, Bool)
    forall a b. (a -> b) -> a -> b
    $
          let preVars :: Set Var
    preVars = [Var] -> Set Var
    forall a. Ord a => [a] -> Set a
    Set.fromList
                [Var
    v | (VarDescr Type t
    _ (Pre t
    _ Var
    v)) <- Map Var VarDescr -> [VarDescr]
    forall k a. Map k a -> [a]
    Map.elems (Map Var VarDescr -> [VarDescr]) -> Map Var VarDescr -> [VarDescr]
    forall a b. (a -> b) -> a -> b
    $ Node -> Map Var VarDescr
    nodeLocalVars Node
    n]
          in Set Var
    preVars Set Var -> Set Var -> Bool
    forall a. Ord a => Set a -> Set a -> Bool
    `isSubsetOf` Node -> Set Var
    nodeLocalVarsSet Node
    n
        ]

    specNodesIds :: TransSys -> Set NodeId
    specNodesIds :: TransSys -> Set NodeId
    specNodesIds TransSys
    s = [NodeId] -> Set NodeId
    forall a. Ord a => [a] -> Set a
    Set.fromList ([NodeId] -> Set NodeId)
    -> ([Node] -> [NodeId]) -> [Node] -> Set NodeId
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Node -> NodeId) -> [Node] -> [NodeId]
    forall a b. (a -> b) -> [a] -> [b]
    map Node -> NodeId
    nodeId ([Node] -> Set NodeId) -> [Node] -> Set NodeId
    forall a b. (a -> b) -> a -> b
    $ TransSys -> [Node]
    specNodes TransSys
    s

    -- | Given a modular transition system, produce a map from each node to its
    -- dependencies.
    specDependenciesGraph :: TransSys -> Map NodeId [NodeId]
    specDependenciesGraph :: TransSys -> Map NodeId [NodeId]
    specDependenciesGraph TransSys
    s =
      [(NodeId, [NodeId])] -> Map NodeId [NodeId]
    forall k a. Ord k => [(k, a)] -> Map k a
    Map.fromList [ (Node -> NodeId
    nodeId Node
    n, Node -> [NodeId]
    nodeDependencies Node
    n) | Node
    n <- TransSys -> [Node]
    specNodes TransSys
    s ]

    -- | Return the top node of a modular transition system.
    specTopNode :: TransSys -> Node
    specTopNode :: TransSys -> Node
    specTopNode TransSys
    spec = Maybe Node -> Node
    forall a. HasCallStack => Maybe a -> a
    fromJust (Maybe Node -> Node) -> Maybe Node -> Node
    forall a b. (a -> b) -> a -> b
    $ (Node -> Bool) -> [Node] -> Maybe Node
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
    List.find
      ((NodeId -> NodeId -> Bool
    forall a. Eq a => a -> a -> Bool
    == TransSys -> NodeId
    specTopNodeId TransSys
    spec) (NodeId -> Bool) -> (Node -> NodeId) -> Node -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Node -> NodeId
    nodeId)
      (TransSys -> [Node]
    specNodes TransSys
    spec)

    instance HasInvariants TransSys where

      invariants :: TransSys -> [(NodeId, Bool)]
    invariants TransSys
    s =
        [ NodeId -> Bool -> (NodeId, Bool)
    prop NodeId
    "All mentioned nodes are declared" (Bool -> (NodeId, Bool)) -> Bool -> (NodeId, Bool)
    forall a b. (a -> b) -> a -> b
    $
          TransSys -> NodeId
    specTopNodeId TransSys
    s NodeId -> Set NodeId -> Bool
    forall a. Ord a => a -> Set a -> Bool
    `member` TransSys -> Set NodeId
    specNodesIds TransSys
    s
          Bool -> Bool -> Bool
    && [NodeId] -> Set NodeId
    forall a. Ord a => [a] -> Set a
    Set.fromList [NodeId
    nId | Node
    n <- TransSys -> [Node]
    specNodes TransSys
    s, NodeId
    nId <- Node -> [NodeId]
    nodeDependencies Node
    n]
             Set NodeId -> Set NodeId -> Bool
    forall a. Ord a => Set a -> Set a -> Bool
    `isSubsetOf` TransSys -> Set NodeId
    specNodesIds TransSys
    s

        , NodeId -> Bool -> (NodeId, Bool)
    prop NodeId
    "The imported vars are not broken" (Bool -> (NodeId, Bool)) -> Bool -> (NodeId, Bool)
    forall a b. (a -> b) -> a -> b
    $
          [Set ExtVar] -> Set ExtVar
    forall a. Monoid a => [a] -> a
    mconcat ((Node -> Set ExtVar) -> [Node] -> [Set ExtVar]
    forall a b. (a -> b) -> [a] -> [b]
    map Node -> Set ExtVar
    nodeImportedExtVarsSet ([Node] -> [Set ExtVar]) -> [Node] -> [Set ExtVar]
    forall a b. (a -> b) -> a -> b
    $ TransSys -> [Node]
    specNodes TransSys
    s) Set ExtVar -> Set ExtVar -> Bool
    forall a. Ord a => Set a -> Set a -> Bool
    `isSubsetOf`
          [Set ExtVar] -> Set ExtVar
    forall a. Monoid a => [a] -> a
    mconcat ((Node -> Set ExtVar) -> [Node] -> [Set ExtVar]
    forall a b. (a -> b) -> [a] -> [b]
    map Node -> Set ExtVar
    nodeExportedExtVarsSet ([Node] -> [Set ExtVar]) -> [Node] -> [Set ExtVar]
    forall a b. (a -> b) -> a -> b
    $ TransSys -> [Node]
    specNodes TransSys
    s)

        , NodeId -> Bool -> (NodeId, Bool)
    prop NodeId
    "The nodes invariants hold" (Bool -> (NodeId, Bool)) -> Bool -> (NodeId, Bool)
    forall a b. (a -> b) -> a -> b
    $ (Node -> Bool) -> [Node] -> Bool
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
    all Node -> Bool
    forall a. HasInvariants a => a -> Bool
    checkInvs (TransSys -> [Node]
    specNodes TransSys
    s)
        ]

    -- | True if the graph is topologically sorted (i.e., if the dependencies of a
    -- node appear in the list of 'specNodes' before the node that depends on
    -- them).
    isTopologicallySorted :: TransSys -> Bool
    isTopologicallySorted :: TransSys -> Bool
    isTopologicallySorted TransSys
    spec =
      Maybe (Set NodeId) -> Bool
    forall a. Maybe a -> Bool
    isJust (Maybe (Set NodeId) -> Bool) -> Maybe (Set NodeId) -> Bool
    forall a b. (a -> b) -> a -> b
    $ (Set NodeId -> Node -> Maybe (Set NodeId))
    -> Set NodeId -> [Node] -> Maybe (Set NodeId)
    forall (t :: * -> *) (m :: * -> *) b a.
    (Foldable t, Monad m) =>
    (b -> a -> m b) -> b -> t a -> m b
    foldM Set NodeId -> Node -> Maybe (Set NodeId)
    forall {m :: * -> *}.
    (Monad m, Alternative m) =>
    Set NodeId -> Node -> m (Set NodeId)
    inspect Set NodeId
    forall a. Set a
    Set.empty (TransSys -> [Node]
    specNodes TransSys
    spec)
      where
        inspect :: Set NodeId -> Node -> m (Set NodeId)
    inspect Set NodeId
    acc Node
    n = do
          Bool -> m ()
    forall (f :: * -> *). Alternative f => Bool -> f ()
    guard (Bool -> m ()) -> Bool -> m ()
    forall a b. (a -> b) -> a -> b
    $ [NodeId] -> Set NodeId
    forall a. Ord a => [a] -> Set a
    Set.fromList (Node -> [NodeId]
    nodeDependencies Node
    n) Set NodeId -> Set NodeId -> Bool
    forall a. Ord a => Set a -> Set a -> Bool
    `isSubsetOf` Set NodeId
    acc
          Set NodeId -> m (Set NodeId)
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Set NodeId -> m (Set NodeId))
    -> (Set NodeId -> Set NodeId) -> Set NodeId -> m (Set NodeId)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . NodeId -> Set NodeId -> Set NodeId
    forall a. Ord a => a -> Set a -> Set a
    Set.insert (Node -> NodeId
    nodeId Node
    n) (Set NodeId -> m (Set NodeId)) -> Set NodeId -> m (Set NodeId)
    forall a b. (a -> b) -> a -> b
    $ Set NodeId
    acc

    -- For debugging purposes
    instance Show ExtVar where
      show :: ExtVar -> NodeId
    show (ExtVar NodeId
    n Var
    v) = NodeId
    "(" NodeId -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ NodeId
    n NodeId -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ NodeId
    " : " NodeId -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ Var -> NodeId
    forall a. Show a => a -> NodeId
    show Var
    v NodeId -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ NodeId
    ")"