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

{-# LANGUAGE Safe #-}

-- | Each prover first translates the Copilot specification into an
-- intermediate representation best suited for model checking.
--
-- This module and the ones in the same namespace implement the TransSys
-- format. A Copilot program is /flattened/ and translated into a /state/
-- /transition system/.  In order to keep some structure in this
-- representation, the variables of this system are grouped by /nodes/, each
-- node exporting and importing variables. The /Kind2 prover/ uses this format,
-- which can be easily translated into the native format.
module Copilot.Theorem.TransSys (module X) where

import Copilot.Theorem.TransSys.Spec as X
import Copilot.Theorem.TransSys.PrettyPrint as X
import Copilot.Theorem.TransSys.Translate as X
import Copilot.Theorem.TransSys.Transform as X

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