copilot-theorem 4.7.1 → 4.8

raw patch · 8 files changed

+228/−195 lines, 8 filesdep +extradep −xmldep ~copilot-coredep ~copilot-prettyprinterPVP ok

version bump matches the API change (PVP)

Dependencies added: extra

Dependencies removed: xml

Dependency ranges changed: copilot-core, copilot-prettyprinter

API changes (from Hackage documentation)

Files

• CHANGELOG +4/−0
• README.md +26/−14
• copilot-theorem.cabal +4/−4
• src/Copilot/Theorem/Kind2/AST.hs +39/−12
• src/Copilot/Theorem/Kind2/Output.hs +74/−43
• src/Copilot/Theorem/Kind2/PrettyPrint.hs +35/−14
• src/Copilot/Theorem/Kind2/Prover.hs +9/−7
• src/Copilot/Theorem/Kind2/Translate.hs +37/−101

@@ -1,3 +1,7 @@+2026-07-07+        * Version bump (4.8). (#745)+        * Extend range of versions of Kind2. (#734)+ 2026-05-07         * Version bump (4.7.1). (#730)         * Handle special Float values correctly for counterexamples. (#697)

@@ -31,7 +31,8 @@ * The *copilot-core* and *copilot-prettyprinter* Haskell libraries * The *Yices2* SMT-solver: `yices-smt2` must be in your `$PATH` * The *Z3* SMT-solver: `z3` must be in your `$PATH`-* The *Kind2* model checker: `kind2` must be in your `$PATH`+* The *Kind2* model checker (version 1.0 or newer): `kind2` must be in your+  `$PATH`  To build it, just install the Copilot library as described in the top-level README.@@ -87,7 +88,9 @@ The *Kind2* prover uses the model checker with the same name, from the University of Iowa. It translates the Copilot specification into a *modular transition system* (the Kind2 native format) and then calls the `kind2`-executable.+executable. Kind2 version 1.0 or newer is required: the native input format+and the command-line options used by this prover were introduced in Kind2+1.0, and remain supported as of Kind2 3.0.  It is provided by the `Copilot.Theorem.Kind2` module, which exports a `kind2Prover :: Options -> Prover` where the `Options` type is defined as@@ -95,7 +98,7 @@ ```haskell data Options = Options { bmcMax :: Int } ```-and where `bmcMax` corresponds to the `--bmc_max` option of *kind2* and is+and where `bmcMax` corresponds to the `--unroll_max` option of *kind2* and is equivalent to the `maxK` option of the K-Induction prover. Its default value is 0, which stands for infinity. @@ -335,11 +338,16 @@  The transition system obtained by the `TransSys.Translate` module is perfectly consistent. However, it can't be directly translated into the *Kind2 native-file format*. Indeed, it is natural to bind each node to a predicate but the-Kind2 file format requires that each predicate only uses previously defined-predicates. However, some nodes in our transition system could be mutually-recursive. Therefore, the goal of the `removeCycles :: Spec -> Spec` function,-defined in `TransSys.Transform`, is to remove such dependency cycles.+file format*. The native input format of Kind2 (version 1.0 and newer) does+not support predicate calls inside the initial state and transition relation+predicates of a node, so the modular structure of the transition system cannot+be expressed directly in it. Therefore, the system is first turned into an+equivalent non-modular transition system with only one node by the+`inline :: Spec -> Spec` function, defined in `TransSys.Transform`:+```haskell+inline :: Spec -> Spec+inline spec = mergeNodes [nodeId n | n <- specNodes spec] spec+```  This function relies on the `mergeNodes :: [NodeId] -> Spec -> Spec` function, whose signature is self-explicit. The latter solves name conflicts by using the@@ -516,10 +524,14 @@ #### Displaying counterexamples  Counterexamples are not displayed with the Kind2 prover because Kind2 doesn't-support XML output of counterexamples. If the last feature is provided, it-should be easy to implement displaying of counterexamples in *copilot-theorem*.-For this, we recommend keeping some information about *observers* in-`TransSys.Spec` and to add one variable per observer in the Kind2 output file.+support the output of counterexamples for systems expressed in its native input+format (the counterexample printing functions in Kind2's+[`src/inputSystem.ml`](https://github.com/kind2-mc/kind2/blob/v3.0.0/src/inputSystem.ml)+fail with an internal error for native input). If Kind2 adds this feature, it+should be easy to implement displaying of counterexamples in+*copilot-theorem*.  For this, we recommend keeping some information about+*observers* in `TransSys.Spec` and to add one variable per observer in the+Kind2 output file.  #### Bad handling of non-linear operators and external functions @@ -569,14 +581,14 @@  It is true that the code of `TransSys` is quite complex. In fact, it would be really straightforward to produce a flattened transition system and then a-Kind2 file with just a single *top* predicate. In fact, It would be as easy as+Kind2 file with just a single *top* node. In fact, It would be as easy as producing an *IL* specification.  To be honest, I'm not sure producing a modular *Kind2* output is worth the complexity added. It's especially true at the time I write this in the sense that: -* Each predicate introduced is used only one time (which is true because+* Each node introduced is used only one time (which is true because   Copilot doesn't handle functions or parameterized streams like Lustre does   and everything is inlined during the reification process). * A similar form of structure could be obtained from a flattened Kind2 native

@@ -14,7 +14,7 @@   <https://copilot-language.github.io>.  -version                   : 4.7.1+version                   : 4.8 license                   : BSD3 license-file              : LICENSE maintainer                : Ivan Perez <ivan.perezdominguez@nasa.gov>@@ -51,6 +51,7 @@                           , containers            >= 0.4 && < 0.9                           , data-default          >= 0.7 && < 0.9                           , directory             >= 1.3 && < 1.4+                          , extra                 >= 1.7 && < 1.9                           , fp-ieee               >= 0.1 && < 0.2                           , libBF                 >= 0.6.2 && < 0.7                           , mtl                   >= 2.0 && < 2.4@@ -60,11 +61,10 @@                           , process               >= 1.6 && < 1.7                           , random                >= 1.1 && < 1.4                           , transformers          >= 0.5 && < 0.7-                          , xml                   >= 1.3 && < 1.4                           , what4                 >= 1.3 && < 1.8 -                          , copilot-core          >= 4.7.1 && < 4.8-                          , copilot-prettyprinter >= 4.7.1 && < 4.8+                          , copilot-core          >= 4.8 && < 4.9+                          , copilot-prettyprinter >= 4.8 && < 4.9    exposed-modules         : Copilot.Theorem                           , Copilot.Theorem.Prove

@@ -1,27 +1,54 @@ {-# LANGUAGE Safe #-} --- | Abstract syntax tree of Kind2 files.+-- | Abstract syntax tree of Kind2 native input files.+--+-- This represents the native transition system input format supported by+-- Kind2 1.0 and newer (@--input_format native@), in which a file is a+-- sequence of @define-node@ forms, each declaring a state transition system+-- by means of an initial state predicate and a transition relation predicate.+-- The last node defined in a file is the top system analyzed by Kind2, and+-- the properties to check are attached to it.+--+-- The native input format is largely undocumented, and Kind2's user+-- documentation only covers its Lustre frontend. The best available+-- references for the native format are the parser in the Kind2 sources+-- ([nativeInput.ml]+-- (https://github.com/kind2-mc/kind2/blob/v3.0.0/src/nativeInput.ml)),+-- which includes a sketch of the grammar in a comment near the end of the+-- file) and the example file+-- [two_counters.kind2]+-- (https://github.com/kind2-mc/kind2/blob/develop/examples/two_counters.kind2). module Copilot.Theorem.Kind2.AST where --- | A file is a sequence of predicates and propositions.+-- | A file is a sequence of node definitions, together with a distinguished+-- top node and a series of propositions about the top node.+--+-- Kind2 analyzes the last node defined in a file as the top system, so the+-- top node is always printed after all the other nodes. data File = File-  { filePreds     :: [PredDef]-  , fileProps     :: [Prop] }+  { fileNodes   :: [Node]  -- ^ Nodes other than the top node, in dependency+                           --   order (a node may only refer to nodes defined+                           --   before it).+  , fileTopNode :: Node    -- ^ The top node, which the propositions are+                           --   attached to.+  , fileProps   :: [Prop]  -- ^ Propositions about the top node.+  }  -- | A proposition is defined by a term. data Prop = Prop   { propName      :: String   , propTerm      :: Term } --- | A predicate definition.-data PredDef = PredDef-  { predId        :: String         -- ^ Identifier for the predicate.-  , predStateVars :: [StateVarDef]  -- ^ Variables identifying the states in the-                                    -- underlying state transition system.-  , predInit      :: Term           -- ^ Predicate that holds for initial+-- | A node definition.+data Node = Node+  { nodeId        :: String         -- ^ Identifier for the node.+  , nodeStateVars :: [StateVarDef]  -- ^ Variables identifying the states in+                                    -- the underlying state transition system.+  , nodeInit      :: Term           -- ^ Predicate that holds for initial                                     -- states.-  , predTrans     :: Term           -- ^ Predicate that holds for two states, if-                                    -- there is state transition between them.+  , nodeTrans     :: Term           -- ^ Predicate that holds for two states,+                                    -- if there is a state transition between+                                    -- them.   }  -- | A definition of a state variable.

@@ -4,66 +4,97 @@ -- | Parse output of Kind2. module Copilot.Theorem.Kind2.Output (parseOutput) where -import Text.XML.Light       hiding (findChild)-import Copilot.Theorem.Prove  as P-import Data.Maybe           (fromJust)+import Data.List.Extra (isInfixOf, splitOn, stripInfix, trim)+import Data.Maybe      (mapMaybe) +import Copilot.Theorem.Prove as P+ import qualified Copilot.Core as C  import qualified Copilot.Theorem.Misc.Error as Err -simpleName s = QName s Nothing Nothing- -- | Parse output of Kind2.+--+-- The output is expected to be in XML format, as produced by Kind2's @-xml@+-- flag and documented at+-- <https://kind.cs.uiowa.edu/kind2_user_doc/3_output/2_machine_readable.html>.+-- Note that this function does not parse the output as XML: when given a+-- system in the native transition system format, Kind2 produces output that+-- is not always well-formed XML (e.g., counterexamples to invariant+-- properties cannot be printed for systems in that format -- the+-- counterexample printing functions in Kind2's @src/inputSystem.ml@ fail with+-- an internal error for native input -- and Kind2 reports the error in the+-- middle of the XML output). Instead, this function looks for the+-- @\<Property\>@ tag for the given property and extracts the answers in the+-- @\<Answer\>@ tags it contains. parseOutput :: String    -- ^ Property whose validity is being checked.             -> C.Prop    -- ^ The property's quantifier.             -> String    -- ^ XML output of Kind2             -> P.Output-parseOutput propId propQuantifier xml = fromJust $ do-  root <- parseXMLDoc xml-  case findAnswer . findPropTag $ root of-    "valid"       -> case propQuantifier of-                       -- We encode a universally quantified property P as-                       -- ∀x.P(x) in Kind2, so the original property is valid-                       -- iff the Kind2 property is valid.-                       C.Forall {} -> return (Output Valid   [])-                       -- We encode an existentially quantified property P as-                       -- ¬(∀x.¬(P(x))) in Kind2, so the original property is-                       -- invalid iff the Kind2 property is valid.-                       C.Exists {} -> return (Output Invalid [])-    "falsifiable" -> case propQuantifier of-                       -- We encode a universally quantified property P as-                       -- ∀x.P(x) in Kind2, so the original property is invalid-                       -- iff the Kind2 property is invalid.-                       C.Forall {} -> return (Output Invalid [])-                       -- We encode an existentially quantified property P as-                       -- ¬(∀x.¬(P(x))) in Kind2, so the original property is-                       -- valid iff the Kind2 property is invalid.-                       C.Exists {} -> return (Output Valid   [])-    s             -> err $ "Unrecognized status : " ++ s+parseOutput propId propQuantifier xml+    | "valid"       `elem` answers = quantified (Output Valid   [])+                                                (Output Invalid [])+    | "falsifiable" `elem` answers = quantified (Output Invalid [])+                                                (Output Valid   [])+    | "unknown"     `elem` answers = Output Unknown []+    | null answers = err $ "Answer for property " ++ propId ++ " not found"+    | otherwise    = err $ "Unrecognized status : " ++ unwords answers    where -    searchForRuntimeError = undefined+    -- Pick an output based on the quantifier of the property. The first+    -- argument is returned when the property Kind2 was asked about is valid,+    -- and the second one when it is invalid.+    --+    -- We encode a universally quantified property P as ∀x.P(x) in Kind2, so+    -- the original property is valid iff the Kind2 property is valid.+    --+    -- We encode an existentially quantified property P as ¬(∀x.¬(P(x))) in+    -- Kind2, so the original property is valid iff the Kind2 property is+    -- invalid.+    quantified ifValid ifInvalid = case propQuantifier of+      C.Forall {} -> ifValid+      C.Exists {} -> ifInvalid -    findPropTag root =-      let rightElement elt =-            qName (elName elt) == "Property"-            && lookupAttr (simpleName "name") (elAttribs elt)-                == Just propId-      in case filterChildren rightElement root of-           tag : _ -> tag-           _ -> err $ "Tag for property " ++ propId ++ " not found"+    -- All the answers reported for the property, in the order in which they+    -- appear in the output. A conclusive answer (valid or falsifiable), if+    -- any, takes precedence over inconclusive (unknown) ones, which Kind2 may+    -- also report when the analysis terminates without an answer for all+    -- properties.+    answers = mapMaybe answerText+            $ filter isRightProperty+            $ propertyElems xml -    findAnswer tag =-      case findChildren (simpleName "Answer") tag of-        answTag : _ ->-          case onlyText (elContent answTag) of-            answ : _ -> cdData answ-            _ -> err "Invalid 'Answer' attribute"-        _ -> err "Attribute 'Answer' not found"+    -- Substrings of the output following a @\<Property @ opening tag, each+    -- extending to the next such tag (or to the end of the output).+    propertyElems = drop 1 . splitOn "<Property " +    -- True if the given property element has the name of the property this+    -- function looks for.+    isRightProperty elem' =+      ("name=\"" ++ escapeAttr propId ++ "\"") `isInfixOf` openingTag+      where+        openingTag = takeWhile (/= '>') elem'++    -- The contents of the first @\<Answer\>@ tag in the given element, if+    -- any.+    answerText elem' = do+      (_, rest)  <- stripInfix "<Answer" elem'+      (_, rest') <- stripInfix ">" rest+      let answer = trim $ takeWhile (/= '<') rest'+      if null answer then Nothing else Just answer+     err :: forall a . String -> a     err msg = Err.fatal $       "Parse error while reading the Kind2 XML output : \n"       ++ msg ++ "\n\n" ++ xml++-- | Escape a string for use as an XML attribute value.+escapeAttr :: String -> String+escapeAttr = concatMap escapeChar+  where+    escapeChar '&' = "&amp;"+    escapeChar '<' = "&lt;"+    escapeChar '>' = "&gt;"+    escapeChar '"' = "&quot;"+    escapeChar c   = [c]

@@ -1,6 +1,8 @@ {-# LANGUAGE Safe #-} --- | Pretty print a Kind2 file defining predicates and propositions.+-- | Pretty print a Kind2 file defining nodes and propositions, in the native+-- transition system input format supported by Kind2 1.0 and newer (see+-- "Copilot.Theorem.Kind2.AST" for pointers to references on the format). module Copilot.Theorem.Kind2.PrettyPrint ( prettyPrint ) where  import Copilot.Theorem.Misc.SExpr@@ -15,6 +17,14 @@ -- | Reserved keyword prime. kwPrime = "prime" +-- | Dummy position attached to the properties of the file.+--+-- Kind2 requires a position (in the format @file:row-col@) for properties+-- declared with the @:user@ source annotation, and reports that position back+-- in its output.+propPosition :: String+propPosition = "copilot:1-1"+ -- | Pretty print a Kind2 file. prettyPrint :: File -> String prettyPrint =@@ -29,30 +39,41 @@ shouldIndent _                          = True  -- | Convert a file into a sequence of expressions.+--+-- The top node is printed last, since Kind2 analyzes the last node of the+-- file as the top system. The properties of the file are attached to it. ppFile :: File -> [SSExpr]-ppFile (File preds props) = map ppPredDef preds ++ ppProps props+ppFile (File nodes top props) =+  map (`ppNode` []) nodes ++ [ppNode top (ppProps props)] --- | Convert a sequence of propositions into command to check each of them.+-- | Convert a sequence of propositions into a props field. ppProps :: [Prop] -> [SSExpr]-ppProps ps = [ node "check-prop" [ list $ map ppProp ps ] ]+ppProps [] = []+ppProps ps = [ node "props" [ list $ map ppProp ps ] ]  -- | Convert a proposition into an expression. ppProp :: Prop -> SSExpr-ppProp (Prop n t) = list [atom n, ppTerm t]+ppProp (Prop n t) = list [atom n, ppTerm t, atom ":user", atom propPosition] --- | Convert a predicate into an expression.-ppPredDef :: PredDef -> SSExpr-ppPredDef pd =-  list [ atom "define-pred"-       , atom (predId pd)-       , list . map ppStateVarDef . predStateVars $ pd-       , node "init"  [ppTerm $ predInit  pd]-       , node "trans" [ppTerm $ predTrans pd] ]+-- | Convert a node, together with optional extra fields, into an expression.+ppNode :: Node -> [SSExpr] -> SSExpr+ppNode n extraFields =+  list $ [ atom "define-node"+         , atom (nodeId n)+         , list . map ppStateVarDef . nodeStateVars $ n+         , node "init"  [ppTerm $ nodeInit  n]+         , node "trans" [ppTerm $ nodeTrans n] ]+         ++ extraFields  -- | Convert a state variable definition into an expression. ppStateVarDef :: StateVarDef -> SSExpr ppStateVarDef svd =-  list [atom (varId svd), ppType (varType svd)]+  list $ [atom (varId svd), ppType (varType svd)]+         ++ map ppStateVarFlag (varFlags svd)++-- | Convert a state variable option into an expression.+ppStateVarFlag :: StateVarFlag -> SSExpr+ppStateVarFlag FConst = atom ":const"  -- | Convert a type into an expression. ppType :: Type -> SSExpr

@@ -28,7 +28,8 @@ -- | Options for Kind2 data Options = Options   { bmcMax :: Int -- ^ Upper bound on the number of unrolling that base and-                  --   step will perform. A value of 0 means /unlimited/.+                  --   step will perform (passed to Kind2 via its+                  --   @--unroll_max@ option). A value of 0 means /unlimited/.   }  -- | Default options with unlimited unrolling for base and step.@@ -41,7 +42,10 @@  -- | A prover backend based on Kind2. ----- The executable @kind2@ must exist and its location be in the @PATH@.+-- The executable @kind2@ must exist and its location be in the @PATH@. Kind2+-- version 1.0 or newer is required: the native input format and the+-- command-line options this prover uses were introduced in Kind2 1.0, and+-- remain supported as of Kind2 3.0. kind2Prover :: Options -> Prover kind2Prover opts = Prover   { proverName =  "Kind2"@@ -50,23 +54,21 @@   , closeProver  = const $ return () }  kind2Prog        = "kind2"-kind2BaseOptions = ["--input-format", "native", "-xml"]+kind2BaseOptions = ["--input_format", "native", "-xml"]  askKind2 :: ProverST -> [PropId] -> [PropId] -> IO Output askKind2 (ProverST opts spec) assumptions toCheck = do -  let kind2Input = prettyPrint . toKind2 Inlined assumptions toCheck $ spec+  let kind2Input = prettyPrint . toKind2 assumptions toCheck $ spec    (tempName, tempHandle) <- openTempFile "." "out" "kind"   hPutStr tempHandle kind2Input   hClose tempHandle    let kind2Options =-        kind2BaseOptions ++ ["--bmc_max", show $ bmcMax opts, tempName]+        kind2BaseOptions ++ ["--unroll_max", show $ bmcMax opts, tempName]    (_, output, _) <- readProcessWithExitCode kind2Prog kind2Options ""--  putStrLn kind2Input    removeFile tempName 

@@ -1,68 +1,44 @@-{-# LANGUAGE GADTs          #-}-{-# LANGUAGE NamedFieldPuns #-}-{-# LANGUAGE RankNTypes     #-}-{-# LANGUAGE Safe           #-}-{-# LANGUAGE ViewPatterns   #-}+{-# LANGUAGE GADTs      #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE Safe       #-}  -- | Convert modular transition systems ('TransSys') into Kind2 file -- specifications. module Copilot.Theorem.Kind2.Translate   ( toKind2-  , Style (..)   ) where  import Copilot.Theorem.TransSys import qualified Copilot.Theorem.Kind2.AST as K -import Control.Exception.Base (assert)- import Data.Function (on) import Data.Maybe (fromJust) -import Data.List (sort, sortBy)-import Data.Map (Map, (!))+import Data.List (partition, sort, sortBy)+import Data.Map ((!))  import qualified Data.Map as Map import qualified Data.Bimap as Bimap --- The following properties MUST hold for the given transition system :--- * Nodes are sorted by topological order--- * Nodes are `completed`, which means the dependency graph is transitive---   and each node imports all the local variables of its dependencies-----type DepGraph = Map NodeId [NodeId]---- | Style of the Kind2 files produced: modular (with multiple separate nodes),--- or all inlined (with only one node).------ In the modular style, the graph is simplified to remove cycles by collapsing--- all nodes participating in a strongly connected components.------ In the inlined style, the structure of the modular transition system is--- discarded and the graph is first turned into a /non-modular transition/--- /system/ with only one node, which can be then converted into a Kind2 file.-data Style = Inlined | Modular- -- | Produce a Kind2 file that checks the properties specified.-toKind2 :: Style     -- ^ Style of the file (modular or inlined).-        -> [PropId]  -- ^ Assumptions+toKind2 :: [PropId]  -- ^ Assumptions         -> [PropId]  -- ^ Properties to be checked         -> TransSys  -- ^ Modular transition system holding the system spec         -> K.File-toKind2 style assumptions checkedProps spec =-  addAssumptions spec assumptions-  $ trSpec (complete spec') predCallsGraph assumptions checkedProps+toKind2 assumptions checkedProps spec =+  addAssumptions spec' assumptions $ trSpec spec' checkedProps   where-    predCallsGraph = specDependenciesGraph spec'-    spec' = case style of-      Inlined -> inline spec-      Modular -> removeCycles spec+    spec' = inline spec -trSpec :: TransSys -> DepGraph -> [PropId] -> [PropId] -> K.File-trSpec spec predCallsGraph _assumptions checkedProps = K.File preds props+trSpec :: TransSys -> [PropId] -> K.File+trSpec spec checkedProps = K.File otherNodes topNode props   where-    preds = map (trNode spec predCallsGraph) (specNodes spec)+    (topNode, otherNodes) =+      case partition ((== specTopNodeId spec) . K.nodeId) nodes of+        ([top], others) -> (top, others)+        _ -> error $ "Kind2.Translate: top node "+                       ++ specTopNodeId spec ++ " not found"+    nodes = map (trNode spec) (specNodes spec)     props = map trProp $       filter ((`elem` checkedProps) . fst) $         Map.toList $ Map.map fst $ specProps spec@@ -70,37 +46,30 @@ trProp :: (PropId, ExtVar) -> K.Prop trProp (pId, var) = K.Prop pId (trVar . extVarLocalPart $ var) -trNode :: TransSys -> DepGraph -> Node -> K.PredDef-trNode spec predCallsGraph node =-  K.PredDef { K.predId, K.predStateVars, K.predInit, K.predTrans }-  where-    predId = nodeId node-    predStateVars = gatherPredStateVars spec node-    predInit  = mkConj $ initLocals  node-                         ++ map (trExpr False) (nodeConstrs node)-                         ++ predCalls True spec predCallsGraph node-    predTrans = mkConj $ transLocals node-                         ++ map (trExpr True) (nodeConstrs node)-                         ++ predCalls False spec predCallsGraph node+trNode :: TransSys -> Node -> K.Node+trNode spec node = K.Node+  { K.nodeId        = nodeId node+  , K.nodeStateVars = gatherPredStateVars spec node+  , K.nodeInit      = mkConj $ initLocals  node+                               ++ map (trExpr False) (nodeConstrs node)+  , K.nodeTrans     = mkConj $ transLocals node+                               ++ map (trExpr True) (nodeConstrs node)+  } +-- | Add the assumptions to the top node of the file by conjoining the+-- corresponding property variables to its initial state and transition+-- relation predicates. addAssumptions :: TransSys -> [PropId] -> K.File -> K.File-addAssumptions spec assumptions (K.File {K.filePreds, K.fileProps}) =-  K.File (changeTail aux filePreds) fileProps+addAssumptions spec assumptions file =+  file { K.fileTopNode = aux (K.fileTopNode file) }   where-    changeTail f (reverse -> l) = case l of-      []     -> error "impossible"-      x : xs -> reverse $ f x : xs--    aux pred =-      let init'  = mkConj ( K.predInit  pred : map K.StateVar vars )-          trans' = mkConj ( K.predTrans pred : map K.PrimedStateVar vars )-      in pred { K.predInit = init', K.predTrans = trans' }+    aux node =+      let init'  = mkConj ( K.nodeInit  node : map K.StateVar vars )+          trans' = mkConj ( K.nodeTrans node : map K.PrimedStateVar vars )+      in node { K.nodeInit = init', K.nodeTrans = trans' } -    vars =-      let bindings   = nodeImportedVars (specTopNode spec)-          toExtVar a = fst $ fromJust $ Map.lookup a $ specProps spec-          toTopVar (ExtVar nId v) = assert (nId == specTopNodeId spec) v-      in map (varName . toTopVar . toExtVar) assumptions+    toExtVar a = fst $ fromJust $ Map.lookup a $ specProps spec+    vars = map (varName . extVarLocalPart . toExtVar) assumptions  -- The ordering really matters here because the variables -- have to be given in this order in a pred call@@ -168,39 +137,6 @@         Pre _ v' -> [mkEquality (trPrimedVar v) (trVar v')]         Expr e   -> [mkEquality (trPrimedVar v) (trExpr True e)]         Constrs cs  -> map (trExpr True) cs--predCalls :: Bool -> TransSys -> DepGraph -> Node -> [K.Term]-predCalls isInitCall spec predCallsGraph node =-  map mkCall toCall-  where-    nid = nodeId node-    toCall = predCallsGraph ! nid-    nodesMap = Map.fromList [(nodeId n, n) | n <- specNodes spec]--    nodeLocals n =-      map (ExtVar n) . sort . Map.keys-      . nodeLocalVars $ (nodesMap ! n)--    mkCall callee-      | isInitCall =-          K.PredApp callee K.Init (argsSeq trVar)-      | otherwise  =-          K.PredApp callee K.Trans (argsSeq trVar ++ argsSeq trPrimedVar)-      where--        calleeLocals = nodeLocals callee-        calleeImported =-          (concatMap nodeLocals . sort . nodeDependencies) $ nodesMap ! callee--        localAlias trVarF ev =-          case Bimap.lookupR ev $ nodeImportedVars node of-            Nothing -> error $-              "This spec is not complete : "-              ++ show ev ++ " should be imported in " ++ nid-            Just v -> trVarF v--        argsSeq trVarF =-          map (localAlias trVarF) (calleeLocals ++ calleeImported)  trExpr :: Bool -> Expr t -> K.Term trExpr primed = tr