result.txt

+- Literate Unit-B Test Suite
|  +- Unit-B Document
|  |  +- basic syntax and scopes
|  |  +- Specification and refinement of a lock-free algorithm
|  |  |  +- test 0, verification, specification with intervals
|  |  |  +- test 1, verification, failed proof with intervals
|  |  |  +- test 2, error message name clash in guards
|  |  |  +- test 3, verification, looking up function outside of domain
|  |  |  +- test 4, m1, liveness implemented with conditional behavior
|  |  |  +- test 5, transient, two branches, enablement of non-empty
|  |  |  +- test 6, transient, two branches, enablement of empty
|  |  |  +- test 7, transient, two branches, negation of empty
|  |  |  +- test 8, transient, two branches, negation of non-empty
|  |  |  +- test 9, transient, two branches, follow and disjunction
|  |  |  +- test 10, duplicate refinement of liveness properties
|  |  |  +- test 11, missing witness
|  |  |  +- test 12, carrier sets without using sets
|  |  |  +- test 13, event splitting
|  |  |  +- test 14, event splitting, event sets
|  |  |  +- test 15, event splitting, expression sets
|  |  |  +- test 16, event splitting, index decl
|  |  |  +- test 17, empty parameter list
|  |  |  +- test 18, empty list in VarScope
|  |  |  +- test 19, splitting POs
|  |  |  +- test 20, Lamport proofs
|  |  |  +- test 21, new index witness
|  |  |  +- test 22, new index proof obligation part a
|  |  |  +- test 23, new index proof obligation part b
|  |  |  +- test 24, scoping in index witness feasibility
|  |  |  +- test 25, parameter promotion and inheritance
|  |  |  +- test 26, scoping problem in sequents
|  |  |  +- test 28, large WD-condition
|  |  |  +- test 29, weakening and splitting / disjunction
|  |  |  +- test 30, weakening and splitting / safety
|  |  |  +- test 31, INIT/fis
|  |  |  +- test 32, inferring used record types
|  |  |  +- test 33, verifying with inferred records
|  |  |  +- test 34, using coarse schedules in proofs of safety of new events
|  |  |  +- test 35, weakened coarse schedule replacement leads-to
|  |  |  +- test 36, deleting indices - AST
|  |  |  +- test 37, deleting indices - PO
|  |  |  +- test 38, deleting indices - verify
|  |  |  +- test 39, deleting indices - Wit FIS
|  |  |  +- test 40, deleting indices - Wit FIS - verify
|  |  |  +- test 41, deleting indices - verify all
|  |  |  +- test 42, use new schedules in proofs of weakening
|  |  |  +- test 43, use new schedules in proofs of weakening, PO
|  |  |  +- test 45, weird error with merging
|  |  |  +- test 46, inconsistent merge event
|  |  |  +- test 47, deleting indices of non-existant event
|  |  |  +- test 48, invariant violation upon index deletion
|  |  |  +- test 49, guard strengthening / merging with index deletion
|  |  |  +- test 50, improper error message
|  |  |  +- test 51, invalid goal for liveness proof
|  |  |  +- test 52, deleted variables are not primed
|  |  |  +- test 53, bad rendering of expressions
|  |  +- [ Success: 52 / 52 ]
|  |  +- small machine example
|  |  |  +- test 0
|  |  |  +- test 1 (separate machine blocks)
|  |  |  +- test 2 (verification, one failure)
|  |  |  +- test 3 (verification)
|  |  |  +- test 4 (proof obligation, invariance)
|  |  |  +- test 5 (co, 'skip' proof obligation)
|  |  |  +- test 6 (verification, coarse schedule stronger than guard)
|  |  |  +- test 7 (schedulability proof obligation)
|  |  |  +- test 8 (schedulability without selecting schedules (trivially true))
|  |  |  +- test 10 (transient PO, enablement)
|  |  |  +- test 11 (transient PO, negation)
|  |  |  +- test 12 name clash between coarse schedule and co properties
|  |  +- [ Success: 12 / 12 ]
|  |  +- Contextual predicate visibility rules
|  |  +- The king and his advisors puzzle
|  |  |  +- puzzle, m0
|  |  |  +- puzzle, m1
|  |  |  +- puzzle, proof obligation
|  |  |  +- puzzle, event visit
|  |  |  +- puzzle, visit enablement, PO
|  |  |  +- puzzle, visit negation, PO
|  |  |  +- puzzle, m2
|  |  |  +- puzzle m3, wd of sums
|  |  |  +- puzzle m3, proofs with sums
|  |  |  +- puzzle, m4
|  |  |  +- puzzle, deleted variables, m3
|  |  |  +- puzzle, deleted variables, m4
|  |  |  +- puzzle, error: invariant referring to deleted variable
|  |  |  +- puzzle, error: assignment to deleted variable
|  |  |  +- test 16, puzzle, removing actions, m3
|  |  |  +- test 17, puzzle, removed actions, m4
|  |  |  +- test 18, simulation proof obligation
|  |  |  +- test 19, simulation proof obligation (init)
|  |  |  +- test 20, crashing proof obligation of invariant with witness
|  |  |  +- test 21, deleting non-existant action
|  |  |  +- test 30, duplicate declarations
|  |  |  +- test 22, error providing a witness for non-deleted variable
|  |  |  +- test 23, error deleting non-existant variable
|  |  |  +- test 24, inherited vs local invariants
|  |  |  +- test 25, error: schedules and guards refer to deleted variables
|  |  |  +- test 27, old guards / new guards
|  |  |  +- test 28, illegal type application
|  |  |  +- test 29, theorem well-definedness
|  |  +- [ Success: 28 / 28 ]
|  |  +- Unless / except clause
|  |  |  +- test 0, unless/except without indices
|  |  |  +- test 1, unless/except with indices and free variables
|  |  +- [ Success: 2 / 2 ]
|  |  +- Unit tests for the parser
|  |  |  +- test 0, phase 1 (structure), create object
|  |  |  +- test 1, phase 1, parsing
|  |  |  +- test 2, phase 2 (variables), creating state
|  |  |  +- test 3, phase 2, parsing
|  |  |  +- test 4, phase 3 (expressions), create object
|  |  |  +- test 5, phase 3, parsing
|  |  |  +- test 6, phase 4 (proofs), create object
|  |  |  +- test 7, phase 4, parsing
|  |  |  +- test 8, make machine
|  |  |  +- QuickCheck inheritance
|  |  +- [ Success: 10 / 10 ]
|  |  +- table of cubes example
|  |  |  +- test 0 (syntax)
|  |  |  +- test 1 (verification)
|  |  |  +- test 2 (init/fis po)
|  |  |  +- proof of inv0
|  |  |  +- empty proof
|  |  +- [ Success: 5 / 5 ]
|  |  +- Specification and refinement of a lock-free algorithm
|  |  |  +- parsing and using definitions
|  |  |  +- proving using definitions
|  |  |  +- invariance proof obligation
|  |  +- [ Success: 3 / 3 ]
|  |  +- train station example
|  |  |  +- part 0
|  |  |  |  +- test 0, syntax
|  |  |  |  +- test 21, multiple imports of sets
|  |  |  +- [ Success: 2 / 2 ]
|  |  |  +- part 1
|  |  |  |  +- test 1, verification
|  |  |  |  +- test 2, proof obligation, enter/fis, in
|  |  |  |  +- test 20, proof obligation, enter/fis, loc
|  |  |  |  +- test 3, proof obligation, leave/fis, in'
|  |  |  |  +- test 19, proof obligation, leave/fis, loc'
|  |  |  |  +- test 4, proof obligation, leave/sch
|  |  |  +- [ Success: 6 / 6 ]
|  |  |  +- part 2
|  |  |  |  +- test 5, proof obligation, leave/en/tr0/WFIS
|  |  |  |  +- test 23, proof obligation, leave/en/tr0/EN
|  |  |  |  +- test 24, proof obligation, leave/en/tr0/NEG
|  |  |  |  +- test 7, undeclared symbol
|  |  |  |  +- test 8, undeclared event (wrt transient)
|  |  |  |  +- test 9, undeclared event (wrt c sched)
|  |  |  +- [ Success: 6 / 6 ]
|  |  |  +- part 3
|  |  |  |  +- test 10, undeclared event (wrt indices)
|  |  |  |  +- test 11, undeclared event (wrt assignment)
|  |  |  |  +- test 12, proof obligation leave/INV/inv2
|  |  |  +- [ Success: 3 / 3 ]
|  |  |  +- part 4
|  |  |  |  +- test 13, verification, name clash between dummy and index
|  |  |  |  +- test 14, verification, non-exhaustive case analysis
|  |  |  |  +- test 15, verification, incorrect new assumption
|  |  |  +- [ Success: 3 / 3 ]
|  |  |  +- part 5
|  |  |  |  +- test 16, verification, proof by parts
|  |  |  |  +- test 17, ill-defined types
|  |  |  |  +- test 18, assertions have type bool
|  |  |  |  +- test 22, missing witness
|  |  |  +- [ Success: 4 / 4 ]
|  |  +- [ Success: 24 / 24 ]
|  |  +- lambda expressions in the cube example
|  |  |  +- part 0
|  |  |  |  +- test 0, verification, lambda vs empty-fun
|  |  |  |  +- test 1, verification, lambda vs ovl, mk-fun
|  |  |  |  +- test 2, verification, lambda vs apply
|  |  |  +- [ Success: 3 / 3 ]
|  |  |  +- part 1
|  |  |  |  +- test 3, verification, set comprehension, failed proof
|  |  |  |  +- test 4, adding a progress property
|  |  |  |  +- test 5, unless properties
|  |  |  +- [ Success: 3 / 3 ]
|  |  |  +- part 2
|  |  |  |  +- test 6, verify progress refinement
|  |  |  |  +- test 7, verify refinement rules
|  |  |  |  +- test 8, verify refinement rules
|  |  |  +- [ Success: 3 / 3 ]
|  |  |  +- part 3
|  |  |  |  +- test 9, verify disjunction rule
|  |  |  |  +- test 10, error: cyclic proof
|  |  |  |  +- test 11, intermediate goals of monotonic simplification
|  |  |  |  +- test 12, bound variable with ambiguous type
|  |  |  |  +- test 13, inv6, PO
|  |  |  +- [ Success: 5 / 5 ]
|  |  +- [ Success: 14 / 14 ]
|  |  +- refinement relations in the phase example
|  |  |  +- test 0, cyclic refinement relation between machines
|  |  |  +- test 1, valid references to variables and event declared in ancestor
|  |  |  +- test 2, invalid proof obligations
|  |  +- [ Success: 3 / 3 ]
|  |  +- train station example, with refinement
|  |  |  +- verify machine m0 (ref)
|  |  |  +- verify machine m1 (ref)
|  |  |  +- Feasibility in m1
|  |  |  +- verify machine m2 (ref)
|  |  |  +- verify machine m2 (ref), in many files
|  |  |  +- cyclic proof of liveness through 3 refinements
|  |  |  +- refinement of undefined machine
|  |  |  +- repeated imports
|  |  +- [ Success: 8 / 8 ]
|  |  +- train station example, with sets
|  |  |  +- verify machine m0 (sets)
|  |  |  +- verify machine m1 (sets)
|  |  |  +- verify machine m2 (sets)
|  |  |  +- m2, enablement proof obligation
|  |  |  +- m2, transient proof obligation, feasibility
|  |  |  +- m2, transient proof obligation, enablement
|  |  |  +- m2, transient proof obligation, negation
|  |  |  +- m2, safety property of schedule replacement
|  |  |  +- verify machine m3 (sets)
|  |  |  +- type checking of boolean expressions
|  |  |  +- verify machine m3 error (wandering free variable)
|  |  |  +- witness well definedness PO
|  |  |  +- PO in m3 (sets)
|  |  +- [ Success: 13 / 13 ]
|  |  +- Garbage collector
|  |  |  +- test0: verify m0
|  |  |  +- test1: verify m1
|  |  |  +- test2: verify m2
|  |  |  +- test3: monotonic simplification
|  |  |  +- test4: monotonicity of POs
|  |  |  +- test5: monotonicity in relation theory
|  |  |  +- test6: monotonicity of POs
|  |  |  +- test7: POs, step 3 (monotonicity, associativity)
|  |  |  +- test8: POs, step 4 (monotonicity, associativity)
|  |  +- [ Success: 9 / 9 ]
|  |  +- Termination Detection
|  |  |  +- test0: verify m0
|  |  |  +- test1: verify m1
|  |  |  +- test2: verify m2
|  |  |  +- test3: verify m3
|  |  |  +- test4: quantified union
|  |  +- [ Success: 5 / 5 ]
|  |  +- Parser
|  |  |  +- test0: verify m0
|  |  |  +- test1: verify m1
|  |  |  +- test2: verify m2
|  |  |  +- test3: spontaneous events
|  |  +- [ Success: 4 / 4 ]
|  |  +- QuickCheck spec of machine parser
|  |  +- the parser is exception free
|  |  +- conformance of instances to type class axioms
|  |  +- expression phase, properties
|  |  +- expression scope, properties
|  |  +- variable scope, properties
|  +- [ Success: 200 / 200 ]
|  +- Unit-B
|  |  +- 0: 'x eventually increases' verifies
|  |  +- 1: train, model 0, verification
|  |  +- 2: train, m0 transient / enablement PO
|  |  +- 3: train, m0 transient / falsification PO
|  |  +- 4: Feasibility and partitioning
|  |  +- 5: Debugging the partitioning
|  |  +- genericity
|  |  |  +- unification, t0
|  |  |  +- unification, t1
|  |  |  +- unification, t2
|  |  |  +- unification, t3
|  |  |  +- unification, t4
|  |  |  +- unification, t5
|  |  |  +- unification, t6
|  |  |  +- type instantiation
|  |  |  +- type inference 1
|  |  |  +- type inference 3
|  |  |  +- type inference 4
|  |  |  +- type inference 5
|  |  |  +- instantiation of unified types is unique
|  |  |  +- common type is symmetric
|  |  |  +- common type is symmetric (counter-example)
|  |  |  +- common type is symmetric (counter-example 2)
|  |  |  +- instantiation of unified types is unique (counter examples)
|  |  |  +- type mapping are acyclic
|  |  |  +- one-point rule simplification on existentials
|  |  |  +- axioms of type classes PreOrd and PartialOrd
|  |  |  +- Record expressions
|  |  |  +- Record sets
|  |  |  +- Record sets in Z3
|  |  |  +- Syntax for record literals
|  |  |  +- Syntax for record update
|  |  |  +- Record syntax: empty record
|  |  |  +- Records: multiple updates
|  |  |  +- Records sets syntax
|  |  |  +- QuasiQuotes with proof monads
|  |  |  +- QuasiQuotes with proof monads and set theory
|  |  |  +- QuasiQuotes with proof monads and assumptions
|  |  |  +- Records lookup syntax
|  |  |  +- Proofs with record lookup
|  |  |  +- Testing the parser (\qforall{x,y}{}{x = y})
|  |  |  +- Testing the parser (\neg (-2) = 2)
|  |  +- [ Success: 35 / 35 ]
|  |  +- 6: unless with except and split event
|  |  +- 7: QuickCheck names
|  +- [ Success: 43 / 43 ]
|  +- latex parser
|  |  +- quickcheck
|  |  +- sample.tex
|  |  +- sorted seq err.tex
|  |  +- reconstitute sample.tex
|  |  +- reconstitute integers.tex
|  |  +- reconstitute sorted seq.tex
|  +- [ Success: 6 / 6 ]
|  +- Z3 test
|  |  +- sample_quant
|  |  +- sample_quant2
|  |  +- sample_quant3
|  |  +- sample proof
|  |  +- canonical lambdas part a
|  |  +- canonical lambdas part b
|  |  +- canonical lambdas with quantifier part a
|  |  +- canonical lambdas with quantifier part b
|  |  +- conversion to first order typing (no type variables)
|  |  +- conversion to first order typing
|  |  +- instantiating type variables by matching some generic types
|  +- [ Success: 11 / 11 ]
|  +- Graphs and operator grammars
|  |  +- case 0 - complete domain of matrices
|  |  +- case 2 - new ambiguities
|  |  +- case 3 - transitive closures
|  |  +- case 4 - transitive closures in linear time
|  |  +- Formatting utilities
|  |  |  +- test 0
|  |  |  +- test 1
|  |  +- [ Success: 2 / 2 ]
|  |  +- case 5 - error monad
|  |  +- case 6 - union of a list of {sorted} list
|  |  +- case 7 - union of a list of {unsorted} list
|  |  +- case 8 - edit distance, random testing
|  |  +- case 9 - edit distance, regression test from random testing
|  |  +- QuickCheck of graphs
|  |  +- case 11 - Relations, quickcheck
|  |  +- case 12 - New graphs, quickcheck
|  |  +- case 13 - Sane line breaks, quickcheck
|  |  +- test 14 - quickcheck brackets
|  |  +- test 15: Generic tuple parsing
|  +- [ Success: 17 / 17 ]
|  +- code generation in the cube example
|  |  +- test0: code for the {state}
|  |  +- test1: code for the {event}
|  |  +- test2: code for the {initialization}
|  |  +- test3: code for the {procedure + loop}
|  |  +- test4: {whole source file}
|  |  +- test5: run {source file}
|  |  +- test6: verify {control flow graph}
|  |  +- test7: {concurrent} code
|  |  +- test8: {run concurrent} code
|  +- [ Success: 9 / 9 ]
|  +- Documentation generation
|  |  +- m2, event m1:moveout
|  |  +- m3, event m1:moveout
|  |  +- safety properties of m2
|  |  +- progress properties of m2
|  |  +- File structure
|  |  +- Root machine
|  |  +- definitions of m2
|  |  +- assumptions of m2
|  +- [ Success: 8 / 8 ]
+- [ Success: 294 / 294 ]

***************
*** SUCCESS ***
***************
Lines of Haskell code:
   14505 total
    1159 src/UnitB/PO.hs
     876 src/Document/Phase/Expressions.hs
     805 src/Document/Phase.hs
     795 src/Document/Visitor.lhs
     645 src/Code/Synthesis.hs
Run time: 2m 20s