Added tests

forge/tests/error/main.rkt

@@ -102,6 +102,8 @@
     (list "failed_unsat.frg" #rx"Failed test")
     (list "failed_sat.frg" #rx"Failed test") 
     ;;; ? after * makes the match lazy, meaning it will match as few characters as possible while still allowing the remainder of the regular expression to match.
+
+    (list "multiple_test_failures.frg" #rx".*?Assertion_All_isRoot_is_necessary_for_isNotRoot failed.*?Invalid example 'thisIsNotATree'.*?Theorem t1 failed")
     (list "properties_undirected_tree_underconstraint_multiple_errors.frg" #rx".*?Assertion_TreeWithEdges_is_necessary_for_isUndirectedTree failed.*?Assertion_All_TreeWithEdges_is_necessary_for_isUndirectedTree failed")
     (list "properties_undirected_tree_overconstraint_error.frg" #rx"Assertion_isUndirected_is_sufficient_for_isUndirectedTree failed.")
     (list "properties_directed_tree_sufficiency_error.frg" #rx"Assertion_All_arethesame_is_sufficient_for_bothRoots failed.")

forge/tests/error/multiple_test_failures.frg

@@ -0,0 +1,37 @@
+#lang forge
+
+option run_sterling off
+option verbose 0
+
+
+sig Node {edges: set Node}
+
+pred isDirectedTree {
+	edges.~edges in iden -- Injective, each child has at most one parent
+	lone edges.Node - Node.edges -- At most one element that does not have a parent
+	no (^edges & iden) -- No loops
+	lone Node or Node in edges.Node + Node.edges -- Either one node or every node has either a child or a parent.
+}
+
+pred isRoot[r : Node] {
+	isDirectedTree
+    one r
+    (some edges) => (r in edges.Node - Node.edges)
+}
+
+pred isNotRoot[n : Node] {
+    isDirectedTree
+    some edges.n
+}
+
+
+assert all r1, r2 : Node | isRoot[r1] is necessary for isNotRoot[r2] 
+
+example thisIsNotATree is {isDirectedTree} for {
+    Node = `Node1
+    edges = `Node1->`Node1
+}
+
+test expect {
+    t1 : {some r1 : Node | isRoot[r1]} is theorem
+}