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

{-# LANGUAGE ExistentialQuantification, GADTs, 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 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.
data TransSys = TransSys
  { TransSys -> [Node]
specNodes         :: [Node]
  , TransSys -> NodeId
specTopNodeId     :: NodeId
  , TransSys -> Map NodeId ExtVar
specProps         :: Map PropId ExtVar }

-- | 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
/= :: Var -> Var -> Bool
$c/= :: Var -> Var -> Bool
== :: Var -> Var -> Bool
$c== :: 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
showList :: [Var] -> ShowS
$cshowList :: [Var] -> ShowS
show :: Var -> NodeId
$cshow :: Var -> NodeId
showsPrec :: Int -> Var -> ShowS
$cshowsPrec :: Int -> 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
min :: Var -> Var -> Var
$cmin :: Var -> Var -> Var
max :: Var -> Var -> Var
$cmax :: Var -> Var -> Var
>= :: Var -> Var -> Bool
$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
compare :: Var -> Var -> Ordering
$ccompare :: Var -> Var -> Ordering
$cp1Ord :: Eq 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
/= :: ExtVar -> ExtVar -> Bool
$c/= :: ExtVar -> ExtVar -> Bool
== :: ExtVar -> ExtVar -> Bool
$c== :: 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
min :: ExtVar -> ExtVar -> ExtVar
$cmin :: ExtVar -> ExtVar -> ExtVar
max :: ExtVar -> ExtVar -> ExtVar
$cmax :: ExtVar -> ExtVar -> ExtVar
>= :: ExtVar -> ExtVar -> Bool
$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
compare :: ExtVar -> ExtVar -> Ordering
$ccompare :: ExtVar -> ExtVar -> Ordering
$cp1Ord :: Eq 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 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 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 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 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 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 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 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 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 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 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 :: Expr t -> Expr t
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 (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 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 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 (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
")"

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