Confusing "No test trace found" error state

[jtremback]

The error state

Err(
    NoTestTraceFound(
        "mc.log",
    ),
)

Is produced by several different error conditions, making debugging hard and confusing. For example:

• It was produced when I forgot an invariant in IBCTests.cfg. In TLC this yielded the much more informative error message The invariant Neg specified in the configuration file is not defined in the specification.
• It is produced when any of the *Test operators in a TLA+ file does not yield an error trace when negated. A single one of the *Test operators in a TLA+ spec not yielding an error trace when negated will result in this error being produced with no indication of which one caused the problem. To find and fix it involves a slow process of trying to negate each *Test operator and seeing if a trace is produced.

[andrey-kuprianov]

Thank you for reporting this, @jtremback! We will fix that.

[rnbguy]

Note. output::parse should parse the whole output for possible error hints.

modelator/modelator/src/module/tlc/output.rs

Lines 8 to 15 in b45faeb

	while let Some(line) = lines.next() {
	// check if found the beginning of the next trace
	if line.starts_with("@!@!@ENDMSG 2121 @!@!@") {
	if let Some(trace) = parse_trace(&mut lines, options)? {
	traces.push(trace);
	}
	}
	}

[rnbguy]

@jtremback I added prelim changes to detect error messages from TLC. Feedbacks are welcome on rnbguy/error branch.

[jtremback]

Oh cool! I'll take a look

[andrey-kuprianov]

Closed via #74