Lines
99.22 %
Functions
87.5 %
Branches
100 %
//! These tests check whether the counter examples generated by the refinement
//! checking procedure are indeed distinguishing. They are located here to avoid
//! circular dependencies.
use std::io::Write;
use merc_syntax::generate_formula;
use merc_vpg::PG;
use rand::rngs::StdRng;
use merc_io::DumpFiles;
use merc_lts::mutate_lts;
use merc_lts::random_lts;
use merc_lts::write_aut;
use merc_utilities::Timing;
use merc_utilities::random_test;
use merc_vpg::solve_zielonka;
use merc_vpg::translate;
use merc_refinement::ExplorationStrategy;
use merc_refinement::RefinementType;
use merc_refinement::refines;
#[test]
#[cfg_attr(miri, ignore)] // Tests are too slow under miri.
fn test_random_trace_refinement() {
random_test(100, |rng| {
is_refinement_test(
"test_random_trace_refinement",
rng,
RefinementType::Trace,
ExplorationStrategy::BFS,
false,
);
});
}
fn test_random_weak_trace_refinement() {
"test_random_weak_trace_refinement",
RefinementType::Weaktrace,
fn test_random_stable_failures_refinement() {
"test_random_stable_failures_refinement",
RefinementType::StableFailures,
fn test_random_failures_divergences_refinement() {
"test_random_failures_divergences_refinement",
RefinementType::FailuresDivergences,
fn test_random_impossible_futures_refinement() {
"test_random_impossible_futures_refinement",
RefinementType::ImpossibleFutures,
fn test_random_trace_refinement_preprocessed() {
true,
fn test_random_weak_trace_refinement_preprocessed() {
"test_random_weak_trace_refinement_preprocessed",
fn test_random_stable_failures_refinement_preprocessed() {
"test_random_stable_failures_refinement_preprocessed",
fn test_random_failures_divergences_refinement_preprocessed() {
"test_random_failures_divergences_refinement_preprocessed",
fn test_random_impossible_futures_refinement_preprocessed() {
"test_random_impossible_futures_refinement_preprocessed",
/// Helper function to define a refinement test that can be instantiated for
/// the various types.
///
/// # Details
/// Internally requests a counter example to be generated, and checks that
/// the counter example is indeed a valid witness for the failure of the
/// refinement check.
fn is_refinement_test(
dump_name: &str,
rng: &mut StdRng,
refinement: RefinementType,
strategy: ExplorationStrategy,
preprocess: bool,
) {
let mut files = DumpFiles::new(dump_name);
let spec_lts = random_lts::<String, _>(rng, 100, 3);
let impl_lts = mutate_lts(&spec_lts, rng, 100).unwrap();
files.dump("spec.aut", |w| write_aut(w, &spec_lts)).unwrap();
files.dump("impl.aut", |w| write_aut(w, &impl_lts)).unwrap();
let mut timing = Timing::default();
let (result, counter_example) = refines(
impl_lts.clone(),
spec_lts.clone(),
refinement,
strategy,
preprocess,
&mut timing,
if !result {
if let Some(ce) = counter_example {
let formula = generate_formula(&ce);
println!("Counter example formula: {}", formula);
files
.dump("counter_example.mcf", |f| Ok(writeln!(f, "{}", formula)?))
.unwrap();
let impl_pg = translate(&impl_lts, &formula).unwrap();
let spec_pg = translate(&spec_lts, &formula).unwrap();
let (impl_solution, _) = solve_zielonka(&impl_pg, false);
let (spec_solution, _) = solve_zielonka(&spec_pg, false);
assert!(
impl_solution[impl_pg.initial_vertex()] != spec_solution[spec_pg.initial_vertex()],
"Refinement returned false, but the counter example is not distinguishing."
} else {
panic!("Expected a counter example.");