closes #758: fixed missing edges in the dependency graph

tlair/src/main/scala/at/forsyte/apalache/tla/lir/transformations/standard/DeclarationSorter.scala

@@ -1,10 +1,12 @@
 package at.forsyte.apalache.tla.lir.transformations.standard
 
-import at.forsyte.apalache.tla.lir.transformations.TlaModuleTransformation
 import at.forsyte.apalache.tla.lir._
 import at.forsyte.apalache.tla.lir.oper.TlaOper
+import at.forsyte.apalache.tla.lir.transformations.TlaModuleTransformation
 import at.forsyte.apalache.tla.lir.transformations.impl.StableTopologicalSort
+import com.typesafe.scalalogging.LazyLogging
 
+import java.io.{FileWriter, PrintWriter}
 import scala.collection.immutable.HashMap
 
 /**
@@ -19,12 +21,13 @@ import scala.collection.immutable.HashMap
  *
  * @author Igor Konnov
  */
-class DeclarationSorter extends TlaModuleTransformation {
+class DeclarationSorter extends TlaModuleTransformation with LazyLogging {
   type Edges = Map[UID, Set[UID]]
+  type MapIdToDecl = Map[UID, TlaDecl]
 
   override def apply(input: TlaModule): TlaModule = {
     // save the original order of the declarations
-    val idToDecl: Map[UID, TlaDecl] = input.declarations.foldLeft(Map.empty[UID, TlaDecl]) { case (map, d) =>
+    val idToDecl: MapIdToDecl = input.declarations.foldLeft(Map.empty[UID, TlaDecl]) { case (map, d) =>
       map + (d.ID -> d)
     }
 
@@ -38,13 +41,44 @@ class DeclarationSorter extends TlaModuleTransformation {
         sorted.map(idToDecl)
 
       case Right(witnesses) =>
+        val filename = explainCyclicDependency(idToDecl, depsGraph, witnesses)
+        logger.error(s"Check the dependency graph in $filename. You can view it with graphviz.")
         val opers = witnesses.map(idToDecl).map(_.name).mkString(", ")
         throw new CyclicDependencyError("Found a cyclic dependency among operators: " + opers)
     }
 
     new TlaModule(input.name, sortedDeclarations)
   }
 
+  // Dump the dependency graph to a dot file. Otherwise, it is very hard to see what is going on.
+  private def explainCyclicDependency(idToDecl: MapIdToDecl, depsGraph: Edges, witnesses: Set[UID]): String = {
+    val filename = "dependencies.dot"
+
+    def getName(uid: UID): String = {
+      idToDecl.get(uid).map(_.name).getOrElse("undefined")
+    }
+
+    def printToDot(writer: PrintWriter): Unit = {
+      writer.println("digraph dependencies {")
+
+      for (fromId <- witnesses) {
+        writer.println("""  n%s[label="%s"];""".format(fromId, getName(fromId)))
+        for (toId <- depsGraph.getOrElse(fromId, Set.empty)) {
+          writer.println("""  n%s -> n%s;""".format(fromId, toId))
+        }
+      }
+      writer.println("}")
+    }
+
+    val writer = new PrintWriter(new FileWriter(filename, false))
+    try {
+      printToDot(writer)
+      filename
+    } finally {
+      writer.close()
+    }
+  }
+
   // For every declaration ID id1, compute the list of distinct ID of the declarations that must be defined before id1
   private def computeDependenciesGraph(declarations: Seq[TlaDecl]): Edges = {
     // create a map from declaration names to their IDs
@@ -86,10 +120,14 @@ class DeclarationSorter extends TlaModuleTransformation {
         // A singleton with the id, if the name is registered; otherwise, empty set.
         nameToId.get(name).fold(Set.empty[UID])(Set(_))
 
-      case OperEx(TlaOper.apply, NameEx(name), _*) =>
+      case OperEx(TlaOper.apply, NameEx(name), args @ _*) =>
         // This may be an application of a user-defined operator.
-        // A singleton with the id, if the name is registered; otherwise, empty set.
-        nameToId.get(name).fold(Set.empty[UID])(Set(_))
+        // A singleton with the id, if the name is registered
+        //   (that is, for a top-level definition); otherwise, return the empty set (that is, for a LET-IN).
+        val base = nameToId.get(name).map(Set(_)).getOrElse(Set.empty)
+        args.foldLeft(base) { (u, arg) =>
+          u ++ usesRec(arg)
+        }
 
       case OperEx(_, args @ _*) =>
         // join the uses of the arguments
@@ -98,7 +136,8 @@ class DeclarationSorter extends TlaModuleTransformation {
         }
 
       case LetInEx(body, decls @ _*) =>
-        // join the uses of the body and the declarations
+        // Join the uses of the body and the declarations.
+        // We do not track dependencies between the LET-IN operators, because they are scoped and ordered.
         decls.foldLeft(usesRec(body)) { (u, d) =>
           u ++ usesRec(d.body)
         }

tlair/src/test/scala/at/forsyte/apalache/tla/lir/transformations/standard/TestDeclarationSorter.scala

@@ -44,6 +44,14 @@ class TestDeclarationSorter extends FunSuite with BeforeAndAfterEach {
     assertThrows[CyclicDependencyError](DeclarationSorter.instance(input))
   }
 
+  test("regression: a cycle hidden via a call") {
+    val foo = tla.declOp("Foo", tla.int(1))
+    val bar = tla.declOp("Bar", tla.appOp(tla.name("Foo"), tla.appOp(tla.name("Baz"))))
+    val baz = tla.declOp("Baz", tla.appOp(tla.name("Foo"), tla.appOp(tla.name("Bar"))))
+    val input = new TlaModule("test", List(foo, bar, baz))
+    assertThrows[CyclicDependencyError](DeclarationSorter.instance(input))
+  }
+
   test("Foo uses VARIABLE x out of order") {
     val foo = tla.declOp("Foo", tla.name("x"))
     val x = TlaVarDecl("x")