Daniel/integration tests improvements

[danwt]

An integration test 'framework' as per #106. I have a basic design.

In one(ish) sentence the design is

Add .tla,.cfg,.rs,.json files to tests/integration/resource/ for each batch of integration tests. The .rs files are where you your Systems for StepRunner and EventRunner style tests live. You must register .json files, as well as the relevant functions inside the .rs files, in tests/integration/main.rs.

Features

• Parallel testing
• Easily isolating 1 test (for debugging)
• Conveniently specifying ModelatorRunTime (ModelChecker) configurations
• Conveniently specifying StepRunner tests
• Conveniently specifying EventRunner tests
• Conveniently specifying Cli tests

Extras

• Now require '--write' flag for cli commands to actually write to disk, otherwise they just the relevant results inside json
• Improves '--help' content for trace cmd by saying that 'n' is the max num counterexamples, partially addressing Error when more tests requested than possible #107

Issues this closes

• Success returned for non-existing tests #108
• Proper integration testing #106

[rnbguy]

CI broke because GH-CI Rust was fetching the latest Clap beta. I fixed the new breaking changes and bumped the version. Everything is fine now.

But some test cases arbitrarily fail on my machine from time to time.

[andrey-kuprianov]

Looks great to me!
We will do some later refinements, but this is a very good first step.

[rnbguy]

Looks like integration tests are failing arbitrarily because sometimes Apalache spits stderr for an arbitrary standard module.

Encountered an exception while attempt to validate /tmp/{{module}}.tla - /tmp/{{module}}.tla (No such file or directory)

This only happens when multiple Apalache runtimes are executed in parallel.

Although, the exit status stays alright. So, handle exit status codes (0, 12, 255) rather than stderr parsing?

[rnbguy]

Also, the tester::tests::test fails arbitrarily.

The problem comes from the race condition to take locks on test_result here and here.

{
    let test_result = Arc::new(Mutex::new(TestResult::Unhandled));
    let old_hook = panic::take_hook();
    panic::set_hook({
        let result = test_result.clone();
        Box::new(move |info| {
            let mut result = result.lock().unwrap();
            let message = match info.payload().downcast_ref::<&'static str>() {
                Some(&s) => s.to_string(),
                None => match info.payload().downcast_ref::<String>() {
                    Some(s) => s.clone(),
                    None => "Unknown error".to_string(),
                },
            };
            let location = match info.location() {
                Some(l) => l.to_string(),
                None => "".to_string(),
            };
            *result = TestResult::Failure { message, location };
        })
    });
    let result = panic::catch_unwind(AssertUnwindSafe(|| test()));
    panic::set_hook(old_hook);
    match result {
        Ok(res) => TestResult::Success(serde_json::to_string_pretty(&res).unwrap()),
        Err(_) => (*test_result.lock().unwrap()).clone(),
    }
}

The code expects the lock from line 179 to happen before the lock from line 198. But it is not guaranteed.

We can use something from std::sync to fix this.

[rnbguy]

I turned off the multi-threaded testing as last resort.

I am merging this to main as these failed tests are not particular to this branch and come from previous commits.

We should refactor the testing framework later.

[rnbguy]

Ready to merge.