use std::fmt;

use std::fs::File;

use std::io::Write;

use std::path::Path;

use merc_syntax::UntypedPbes;

use test_case::test_case;

use merc_syntax::UntypedDataSpecification;

use merc_syntax::UntypedProcessSpecification;

use merc_syntax::UntypedStateFrmSpec;

use merc_utilities::MercError;

use merc_utilities::test_logger;

/// Creates a snapshot of the given object, in JSON format, in the snapshot directory. If the snapshot already exists then

/// the JSON representation of the object is compared to the stored snapshot.

        // Read the existing tests/snapshot and compare it to the given object.

            result, expected_str,

            "Result does not match the stored snapshot at {snapshot_path:?}"

        );

    } else {

        // Write a new snapshot if the file does not exists

    }

#[cfg_attr(miri, ignore)]

#[test_case(include_str!("../../../examples/mCRL2/academic/abp/abp.mcrl2"), "tests/snapshot/result_abp.mcrl2" ; "abp.mcrl2")]

#[test_case(include_str!("../../../examples/mCRL2/academic/abp_bw/abp_bw.mcrl2"), "tests/snapshot/result_abp_bw.mcrl2" ; "abp_bw.mcrl2")]

#[test_case(include_str!("../../../examples/mCRL2/academic/allow/allow.mcrl2"), "tests/snapshot/result_allow.mcrl2" ; "allow.mcrl2")]

#[test_case(include_str!("../../../examples/mCRL2/academic/bakery/bakery.mcrl2"), "tests/snapshot/result_bakery.mcrl2" ; "bakery.mcrl2")]

#[test_case(include_str!("../../../examples/mCRL2/academic/bke/bke.mcrl2"), "tests/snapshot/result_bke.mcrl2" ; "bke.mcrl2")]

#[test_case(include_str!("../../../examples/mCRL2/academic/block/block.mcrl2"), "tests/snapshot/result_block.mcrl2" ; "block.mcrl2")]

#[test_case(include_str!("../../../examples/mCRL2/academic/bounded_ricart-agrawala/RA_fixed/RA_fixed_spec.mcrl2"), "tests/snapshot/result_ra_fixed_spec.mcrl2" ; "ra_fixed_spec.mcrl2")]

#[test_case(include_str!("../../../examples/mCRL2/academic/bounded_ricart-agrawala/RA_fixed+broadcast/RA_fixed+broadcast_spec.mcrl2"), "tests/snapshot/result_ra_fixed+broadcast_spec.mcrl2" ; "ra_fixed+broadcast_spec.mcrl2")]

#[test_case(include_str!("../../../examples/mCRL2/academic/bounded_ricart-agrawala/RA_fixed+reduced/RA_fixed+reduced_spec.mcrl2"), "tests/snapshot/result_ra_fixed+reduced_spec.mcrl2" ; "ra_fixed+reduced_spec.mcrl2")]

#[test_case(include_str!("../../../examples/mCRL2/academic/bounded_ricart-agrawala/RA_original/RA_original_spec.mcrl2"), "tests/snapshot/result_ra_original_spec.mcrl2" ; "ra_original_spec.mcrl2")]

#[test_case(include_str!("../../../examples/mCRL2/academic/cabp/cabp.mcrl2"), "tests/snapshot/result_cabp.mcrl2" ; "cabp.mcrl2")]

#[test_case(include_str!("../../../examples/mCRL2/academic/cellular_automata/cellular_automata.mcrl2"), "tests/snapshot/result_cellular_automata.mcrl2" ; "cellular_automata.mcrl2")]

#[test_case(include_str!("../../../examples/mCRL2/academic/commprot/commprot.mcrl2"), "tests/snapshot/result_commprot.mcrl2" ; "commprot.mcrl2")]

#[test_case(include_str!("../../../examples/mCRL2/academic/dining/dining3.mcrl2"), "tests/snapshot/result_dining3.mcrl2" ; "dining3.mcrl2")]

#[test_case(include_str!("../../../examples/mCRL2/academic/dining/dining3_cs.mcrl2"), "tests/snapshot/result_dining3_cs.mcrl2" ; "dining3_cs.mcrl2")]

#[test_case(include_str!("../../../examples/mCRL2/academic/dining/dining3_cs_seq.mcrl2"), "tests/snapshot/result_dining3_cs_seq.mcrl2" ; "dining3_cs_seq.mcrl2")]

#[test_case(include_str!("../../../examples/mCRL2/academic/dining/dining3_ns.mcrl2"), "tests/snapshot/result_dining3_ns.mcrl2" ; "dining3_ns.mcrl2")]

#[test_case(include_str!("../../../examples/mCRL2/academic/dining/dining3_ns_seq.mcrl2"), "tests/snapshot/result_dining3_ns_seq.mcrl2" ; "dining3_ns_seq.mcrl2")]

#[test_case(include_str!("../../../examples/mCRL2/academic/dining/dining3_schedule.mcrl2"), "tests/snapshot/result_dining3_schedule.mcrl2" ; "dining3_schedule.mcrl2")]

#[test_case(include_str!("../../../examples/mCRL2/academic/dining/dining3_schedule_seq.mcrl2"), "tests/snapshot/result_dining3_schedule_seq.mcrl2" ; "dining3_schedule_seq.mcrl2")]

#[test_case(include_str!("../../../examples/mCRL2/academic/dining/dining3_seq.mcrl2"), "tests/snapshot/result_dining3_seq.mcrl2" ; "dining3_seq.mcrl2")]

#[test_case(include_str!("../../../examples/mCRL2/academic/dining/dining8.mcrl2"), "tests/snapshot/result_dining8.mcrl2" ; "dining8.mcrl2")]

#[test_case(include_str!("../../../examples/mCRL2/academic/dining/dining_10.mcrl2"), "tests/snapshot/result_dining_10.mcrl2" ; "dining_10.mcrl2")]

#[test_case(include_str!("../../../examples/mCRL2/academic/food_distribution/food_package.mcrl2"), "tests/snapshot/result_food_package.mcrl2" ; "food_package.mcrl2")]

#[test_case(include_str!("../../../examples/mCRL2/academic/goback/goback.mcrl2"), "tests/snapshot/result_goback.mcrl2" ; "goback.mcrl2")]

#[test_case(include_str!("../../../examples/mCRL2/academic/hopcroft/hopcroft.mcrl2"), "tests/snapshot/result_hopcroft.mcrl2" ; "hopcroft.mcrl2")]

#[test_case(include_str!("../../../examples/mCRL2/academic/leader/dolev_klawe_rodeh.mcrl2"), "tests/snapshot/result_dolev_klawe_rodeh.mcrl2" ; "dolev_klawe_rodeh.mcrl2")]

#[test_case(include_str!("../../../examples/mCRL2/academic/leader/leader.mcrl2"), "tests/snapshot/result_leader.mcrl2" ; "leader.mcrl2")]

// #[test_case(include_str!("../../../examples/mCRL2/academic/minepump_product_line/family_based_experiments/formula1/mp_fts_prop1.mcrl2"), "tests/snapshot/result_mp_fts_prop1.mcrl2" ; "mp_fts_prop1.mcrl2")]

// #[test_case(include_str!("../../../examples/mCRL2/academic/minepump_product_line/family_based_experiments/formula10/mp_fts_prop10.mcrl2"), "tests/snapshot/result_mp_fts_prop10.mcrl2" ; "mp_fts_prop10.mcrl2")]

// #[test_case(include_str!("../../../examples/mCRL2/academic/minepump_product_line/family_based_experiments/formula11/mp_fts_prop11.mcrl2"), "tests/snapshot/result_mp_fts_prop11.mcrl2" ; "mp_fts_prop11.mcrl2")]

// #[test_case(include_str!("../../../examples/mCRL2/academic/minepump_product_line/family_based_experiments/formula12/mp_fts_prop12.mcrl2"), "tests/snapshot/result_mp_fts_prop12.mcrl2" ; "mp_fts_prop12.mcrl2")]

// #[test_case(include_str!("../../../examples/mCRL2/academic/minepump_product_line/family_based_experiments/formula2/mp_fts_prop2.mcrl2"), "tests/snapshot/result_mp_fts_prop2.mcrl2" ; "mp_fts_prop2.mcrl2")]

// #[test_case(include_str!("../../../examples/mCRL2/academic/minepump_product_line/family_based_experiments/formula3/mp_fts_prop3.mcrl2"), "tests/snapshot/result_mp_fts_prop3.mcrl2" ; "mp_fts_prop3.mcrl2")]

// #[test_case(include_str!("../../../examples/mCRL2/academic/minepump_product_line/family_based_experiments/formula4/mp_fts_prop4.mcrl2"), "tests/snapshot/result_mp_fts_prop4.mcrl2" ; "mp_fts_prop4.mcrl2")]

// #[test_case(include_str!("../../../examples/mCRL2/academic/minepump_product_line/family_based_experiments/formula5/mp_fts_prop5.mcrl2"), "tests/snapshot/result_mp_fts_prop5.mcrl2" ; "mp_fts_prop5.mcrl2")]

// #[test_case(include_str!("../../../examples/mCRL2/academic/minepump_product_line/family_based_experiments/formula6/mp_fts_prop6.mcrl2"), "tests/snapshot/result_mp_fts_prop6.mcrl2" ; "mp_fts_prop6.mcrl2")]

// #[test_case(include_str!("../../../examples/mCRL2/academic/minepump_product_line/family_based_experiments/formula7/mp_fts_prop7.mcrl2"), "tests/snapshot/result_mp_fts_prop7.mcrl2" ; "mp_fts_prop7.mcrl2")]

// #[test_case(include_str!("../../../examples/mCRL2/academic/minepump_product_line/family_based_experiments/formula8/mp_fts_prop8.mcrl2"), "tests/snapshot/result_mp_fts_prop8.mcrl2" ; "mp_fts_prop8.mcrl2")]

// #[test_case(include_str!("../../../examples/mCRL2/academic/minepump_product_line/family_based_experiments/formula9/mp_fts_prop9.mcrl2"), "tests/snapshot/result_mp_fts_prop9.mcrl2" ; "mp_fts_prop9.mcrl2")]

// #[test_case(include_str!("../../../examples/mCRL2/academic/minepump_product_line/minepump_fts.mcrl2"), "tests/snapshot/result_minepump_fts.mcrl2" ; "minepump_fts.mcrl2")]

// #[test_case(include_str!("../../../examples/mCRL2/academic/minepump_product_line/product_based_experiments/formula1/minepump.mcrl2"), "tests/snapshot/result_minepump.mcrl2" ; "minepump.mcrl2")]

#[test_case(include_str!("../../../examples/mCRL2/academic/mpsu/mpsu.mcrl2"), "tests/snapshot/result_mpsu.mcrl2" ; "mpsu.mcrl2")]

#[test_case(include_str!("../../../examples/mCRL2/academic/mutex_models/Dekker/Dekker_spec.mcrl2"), "tests/snapshot/result_dekker_spec.mcrl2" ; "dekker_spec.mcrl2")]

#[test_case(include_str!("../../../examples/mCRL2/academic/mutex_models/Improved-mutex-naive/Improved-mutex-naive_spec.mcrl2"), "tests/snapshot/result_improved-mutex-naive_spec.mcrl2" ; "improved-mutex-naive_spec.mcrl2")]

#[test_case(include_str!("../../../examples/mCRL2/academic/mutex_models/Mutex-naive/Mutex-naive_spec.mcrl2"), "tests/snapshot/result_mutex-naive_spec.mcrl2" ; "mutex-naive_spec.mcrl2")]

#[test_case(include_str!("../../../examples/mCRL2/academic/mutex_models/Petersons/Petersons_spec.mcrl2"), "tests/snapshot/result_petersons_spec.mcrl2" ; "petersons_spec.mcrl2")]

#[test_case(include_str!("../../../examples/mCRL2/academic/mutex_models/Petersons-3/Petersons-3_spec.mcrl2"), "tests/snapshot/result_petersons-3_spec.mcrl2" ; "petersons-3_spec.mcrl2")]

#[test_case(include_str!("../../../examples/mCRL2/academic/non-atomic_registers/Aravind_BLRU/Aravind_BLRU_spec.mcrl2"), "tests/snapshot/result_aravind_blru_spec.mcrl2" ; "aravind_blru_spec.mcrl2")]

#[test_case(include_str!("../../../examples/mCRL2/academic/non-atomic_registers/Attiya-Welch/Attiya-Welch_spec.mcrl2"), "tests/snapshot/result_attiya-welch_spec.mcrl2" ; "attiya-welch_spec.mcrl2")]

#[test_case(include_str!("../../../examples/mCRL2/academic/non-atomic_registers/Attiya-Welch_alternate/Attiya-Welch_alternate_spec.mcrl2"), "tests/snapshot/result_attiya-welch_alternate_spec.mcrl2" ; "attiya-welch_alternate_spec.mcrl2")]

#[test_case(include_str!("../../../examples/mCRL2/academic/non-atomic_registers/Dijkstra/Dijkstra_spec.mcrl2"), "tests/snapshot/result_dijkstra_spec.mcrl2" ; "dijkstra_spec.mcrl2")]

#[test_case(include_str!("../../../examples/mCRL2/academic/non-atomic_registers/Knuth/Knuth_spec.mcrl2"), "tests/snapshot/result_knuth_spec.mcrl2" ; "knuth_spec.mcrl2")]

#[test_case(include_str!("../../../examples/mCRL2/academic/non-atomic_registers/Lamport_3bit/Lamport_3bit_spec.mcrl2"), "tests/snapshot/result_lamport_3bit_spec.mcrl2" ; "lamport_3bit_spec.mcrl2")]

#[test_case(include_str!("../../../examples/mCRL2/academic/non-atomic_registers/Lamport_3bit_incorrect_z/Lamport_3bit_incorrect_z_spec.mcrl2"), "tests/snapshot/result_lamport_3bit_incorrect_z_spec.mcrl2" ; "lamport_3bit_incorrect_z_spec.mcrl2")]

#[test_case(include_str!("../../../examples/mCRL2/academic/non-atomic_registers/Peterson/Peterson_spec.mcrl2"), "tests/snapshot/result_peterson_spec.mcrl2" ; "peterson_spec.mcrl2")]

#[test_case(include_str!("../../../examples/mCRL2/academic/non-atomic_registers/Register_model/Register_model_spec.mcrl2"), "tests/snapshot/result_register_model_spec.mcrl2" ; "register_model_spec.mcrl2")]

#[test_case(include_str!("../../../examples/mCRL2/academic/non-atomic_registers/Szymanski_3bit_linear_wait/Szymanski_3bit_linear_wait_spec.mcrl2"), "tests/snapshot/result_szymanski_3bit_linear_wait_spec.mcrl2" ; "szymanski_3bit_linear_wait_spec.mcrl2")]

#[test_case(include_str!("../../../examples/mCRL2/academic/non-atomic_registers/Szymanski_3bitlw_sem/Szymanski_3bitlw_sem_spec.mcrl2"), "tests/snapshot/result_szymanski_3bitlw_sem_spec.mcrl2" ; "szymanski_3bitlw_sem_spec.mcrl2")]

#[test_case(include_str!("../../../examples/mCRL2/academic/non-atomic_registers/Szymanski_flag/Szymanski_flag_spec.mcrl2"), "tests/snapshot/result_szymanski_flag_spec.mcrl2" ; "szymanski_flag_spec.mcrl2")]

#[test_case(include_str!("../../../examples/mCRL2/academic/non-atomic_registers/Szymanski_flag_with_bits/Szymanski_flag_with_bits_spec.mcrl2"), "tests/snapshot/result_szymanski_flag_with_bits_spec.mcrl2" ; "szymanski_flag_with_bits_spec.mcrl2")]

#[test_case(include_str!("../../../examples/mCRL2/academic/non-atomic_registers/Szymanski_fwb_pe/Szymanski_fwb_pe_spec.mcrl2"), "tests/snapshot/result_szymanski_fwb_pe_spec.mcrl2" ; "szymanski_fwb_pe_spec.mcrl2")]

#[test_case(include_str!("../../../examples/mCRL2/academic/onebit/onebit.mcrl2"), "tests/snapshot/result_onebit.mcrl2" ; "onebit.mcrl2")]

#[test_case(include_str!("../../../examples/mCRL2/academic/par/par.mcrl2"), "tests/snapshot/result_par.mcrl2" ; "par.mcrl2")]

#[test_case(include_str!("../../../examples/mCRL2/academic/parallel/parallel.mcrl2"), "tests/snapshot/result_parallel.mcrl2" ; "parallel.mcrl2")]

#[test_case(include_str!("../../../examples/mCRL2/academic/parallel_proc_with_global_var/parallel_counting.mcrl2"), "tests/snapshot/result_parallel_counting.mcrl2" ; "parallel_counting.mcrl2")]

#[test_case(include_str!("../../../examples/mCRL2/academic/peterson_justness/mutex.mcrl2"), "tests/snapshot/result_mutex.mcrl2" ; "mutex.mcrl2")]

#[test_case(include_str!("../../../examples/mCRL2/academic/producer_consumer/producer_consumer.mcrl2"), "tests/snapshot/result_producer_consumer.mcrl2" ; "producer_consumer.mcrl2")]

#[test_case(include_str!("../../../examples/mCRL2/academic/scheduler/scheduler.mcrl2"), "tests/snapshot/result_scheduler.mcrl2" ; "scheduler.mcrl2")]

#[test_case(include_str!("../../../examples/mCRL2/academic/swp/swp_fgpbp.mcrl2"), "tests/snapshot/result_swp_fgpbp.mcrl2" ; "swp_fgpbp.mcrl2")]

#[test_case(include_str!("../../../examples/mCRL2/academic/swp/swp_func.mcrl2"), "tests/snapshot/result_swp_func.mcrl2" ; "swp_func.mcrl2")]

#[test_case(include_str!("../../../examples/mCRL2/academic/swp/swp_lists.mcrl2"), "tests/snapshot/result_swp_lists.mcrl2" ; "swp_lists.mcrl2")]

#[test_case(include_str!("../../../examples/mCRL2/academic/swp/swp_with_tanenbaums_bug.mcrl2"), "tests/snapshot/result_swp_with_tanenbaums_bug.mcrl2" ; "swp_with_tanenbaums_bug.mcrl2")]

#[test_case(include_str!("../../../examples/mCRL2/academic/trains/trains.mcrl2"), "tests/snapshot/result_trains.mcrl2" ; "trains.mcrl2")]

#[test_case(include_str!("../../../examples/mCRL2/academic/tree/tree.mcrl2"), "tests/snapshot/result_tree.mcrl2" ; "tree.mcrl2")]

#[test_case(include_str!("../../../examples/mCRL2/games/beggar_my_neighbour/beggar_my_neighbour.mcrl2"), "tests/snapshot/result_beggar_my_neighbour.mcrl2" ; "beggar_my_neighbour.mcrl2")]

#[test_case(include_str!("../../../examples/mCRL2/games/bridge_crossing/bridge_crossing.mcrl2"), "tests/snapshot/result_bridge_crossing.mcrl2" ; "bridge_crossing.mcrl2")]

#[test_case(include_str!("../../../examples/mCRL2/games/clobber/clobber.mcrl2"), "tests/snapshot/result_clobber.mcrl2" ; "clobber.mcrl2")]

#[test_case(include_str!("../../../examples/mCRL2/games/domineering/domineering.mcrl2"), "tests/snapshot/result_domineering.mcrl2" ; "domineering.mcrl2")]

#[test_case(include_str!("../../../examples/mCRL2/games/four_in_a_row/four_in_a_row.mcrl2"), "tests/snapshot/result_four_in_a_row.mcrl2" ; "four_in_a_row.mcrl2")]

#[test_case(include_str!("../../../examples/mCRL2/games/four_in_a_row_symbolic/four_in_a_row_symbolic.mcrl2"), "tests/snapshot/result_four_in_a_row_symbolic.mcrl2" ; "four_in_a_row_symbolic.mcrl2")]

#[test_case(include_str!("../../../examples/mCRL2/games/game_of_goose/game_of_goose.mcrl2"), "tests/snapshot/result_game_of_goose.mcrl2" ; "game_of_goose.mcrl2")]

#[test_case(include_str!("../../../examples/mCRL2/games/hex/hex.mcrl2"), "tests/snapshot/result_hex.mcrl2" ; "hex.mcrl2")]

#[test_case(include_str!("../../../examples/mCRL2/games/knights/knights.mcrl2"), "tests/snapshot/result_knights.mcrl2" ; "knights.mcrl2")]

#[test_case(include_str!("../../../examples/mCRL2/games/magic_square/magic_hexagon.mcrl2"), "tests/snapshot/result_magic_hexagon.mcrl2" ; "magic_hexagon.mcrl2")]

#[test_case(include_str!("../../../examples/mCRL2/games/magic_square/magic_square.mcrl2"), "tests/snapshot/result_magic_square.mcrl2" ; "magic_square.mcrl2")]

#[test_case(include_str!("../../../examples/mCRL2/games/open_field_tic_tac_toe/open_field_tictactoe.mcrl2"), "tests/snapshot/result_open_field_tictactoe.mcrl2" ; "open_field_tictactoe.mcrl2")]

#[test_case(include_str!("../../../examples/mCRL2/games/othello/othello.mcrl2"), "tests/snapshot/result_othello.mcrl2" ; "othello.mcrl2")]

#[test_case(include_str!("../../../examples/mCRL2/games/peg_solitaire/peg_solitaire.mcrl2"), "tests/snapshot/result_peg_solitaire.mcrl2" ; "peg_solitaire.mcrl2")]

#[test_case(include_str!("../../../examples/mCRL2/games/quoridor/quoridor.mcrl2"), "tests/snapshot/result_quoridor.mcrl2" ; "quoridor.mcrl2")]

#[test_case(include_str!("../../../examples/mCRL2/games/rubiks_cube/rubiks_cube.mcrl2"), "tests/snapshot/result_rubiks_cube.mcrl2" ; "rubiks_cube.mcrl2")]

#[test_case(include_str!("../../../examples/mCRL2/games/rubiks_cube_small/small_cube.mcrl2"), "tests/snapshot/result_small_cube.mcrl2" ; "small_cube.mcrl2")]

#[test_case(include_str!("../../../examples/mCRL2/games/snake/snake.mcrl2"), "tests/snapshot/result_snake.mcrl2" ; "snake.mcrl2")]

#[test_case(include_str!("../../../examples/mCRL2/games/sokoban/sokoban.mcrl2"), "tests/snapshot/result_sokoban.mcrl2" ; "sokoban.mcrl2")]

#[test_case(include_str!("../../../examples/mCRL2/games/sudoku/sudoku.mcrl2"), "tests/snapshot/result_sudoku.mcrl2" ; "sudoku.mcrl2")]

#[test_case(include_str!("../../../examples/mCRL2/games/tictactoe/tictactoe.mcrl2"), "tests/snapshot/result_tictactoe.mcrl2" ; "tictactoe.mcrl2")]

#[test_case(include_str!("../../../examples/mCRL2/games/tictactoe/tictactoe_fast.mcrl2"), "tests/snapshot/result_tictactoe_fast.mcrl2" ; "tictactoe_fast.mcrl2")]

#[test_case(include_str!("../../../examples/mCRL2/games/wolf_goat_cabbage/wolf_goat_cabbage.mcrl2"), "tests/snapshot/result_wolf_goat_cabbage.mcrl2" ; "wolf_goat_cabbage.mcrl2")]

#[test_case(include_str!("../../../examples/mCRL2/industrial/1394/1394-fin.mcrl2"), "tests/snapshot/result_1394-fin.mcrl2" ; "1394-fin.mcrl2")]

#[test_case(include_str!("../../../examples/mCRL2/industrial/DIRAC/SMS.mcrl2"), "tests/snapshot/result_sms.mcrl2" ; "sms.mcrl2")]

#[test_case(include_str!("../../../examples/mCRL2/industrial/DIRAC/WMS.mcrl2"), "tests/snapshot/result_wms.mcrl2" ; "wms.mcrl2")]

#[test_case(include_str!("../../../examples/mCRL2/industrial/ERTMS/version1A/section_I/IU/ertms-hl3.mcrl2"), "tests/snapshot/result_ertms-hl3.mcrl2" ; "ertms-hl3.mcrl2")]

#[test_case(include_str!("../../../examples/mCRL2/industrial/ERTMS/version1A/section_II/IU/ertms-hl3.announce.mcrl2"), "tests/snapshot/result_ertms-hl3.announce.mcrl2" ; "ertms-hl3.announce.mcrl2")]

// #[test_case(include_str!("../../../examples/mCRL2/industrial/MLV/MLV.mcrl2"), "tests/snapshot/result_mlv.mcrl2" ; "mlv.mcrl2")]

#[test_case(include_str!("../../../examples/mCRL2/industrial/alma/alma.mcrl2"), "tests/snapshot/result_alma.mcrl2" ; "alma.mcrl2")]

#[test_case(include_str!("../../../examples/mCRL2/industrial/brp/brp.mcrl2"), "tests/snapshot/result_brp.mcrl2" ; "brp.mcrl2")]

#[test_case(include_str!("../../../examples/mCRL2/industrial/chatbox/chatbox.mcrl2"), "tests/snapshot/result_chatbox.mcrl2" ; "chatbox.mcrl2")]

#[test_case(include_str!("../../../examples/mCRL2/industrial/flexray/3_Ideal_trace.expanded.mcrl2"), "tests/snapshot/result_3_ideal_trace.expanded.mcrl2" ; "3_ideal_trace.expanded.mcrl2")]

#[test_case(include_str!("../../../examples/mCRL2/industrial/flexray/3_Mute_follower.expanded.mcrl2"), "tests/snapshot/result_3_mute_follower.expanded.mcrl2" ; "3_mute_follower.expanded.mcrl2")]

#[test_case(include_str!("../../../examples/mCRL2/industrial/flexray/3_Mute_leader.expanded.mcrl2"), "tests/snapshot/result_3_mute_leader.expanded.mcrl2" ; "3_mute_leader.expanded.mcrl2")]

#[test_case(include_str!("../../../examples/mCRL2/industrial/flexray/3_Regular.expanded.mcrl2"), "tests/snapshot/result_3_regular.expanded.mcrl2" ; "3_regular.expanded.mcrl2")]

#[test_case(include_str!("../../../examples/mCRL2/industrial/flexray/Big_Deaf_follower.expanded.mcrl2"), "tests/snapshot/result_big_deaf_follower.expanded.mcrl2" ; "big_deaf_follower.expanded.mcrl2")]

#[test_case(include_str!("../../../examples/mCRL2/industrial/garage/garage-r1.mcrl2"), "tests/snapshot/result_garage-r1.mcrl2" ; "garage-r1.mcrl2")]

#[test_case(include_str!("../../../examples/mCRL2/industrial/garage/garage-r2-error.mcrl2"), "tests/snapshot/result_garage-r2-error.mcrl2" ; "garage-r2-error.mcrl2")]

#[test_case(include_str!("../../../examples/mCRL2/industrial/garage/garage-r2.mcrl2"), "tests/snapshot/result_garage-r2.mcrl2" ; "garage-r2.mcrl2")]

#[test_case(include_str!("../../../examples/mCRL2/industrial/garage/garage-r3.mcrl2"), "tests/snapshot/result_garage-r3.mcrl2" ; "garage-r3.mcrl2")]

// #[test_case(include_str!("../../../examples/mCRL2/industrial/garage/garage-ver.mcrl2"), "tests/snapshot/result_garage-ver.mcrl2" ; "garage-ver.mcrl2")]

#[test_case(include_str!("../../../examples/mCRL2/industrial/garage/garage.mcrl2"), "tests/snapshot/result_garage.mcrl2" ; "garage.mcrl2")]

#[test_case(include_str!("../../../examples/mCRL2/industrial/ieee-11073/11073.mcrl2"), "tests/snapshot/result_11073.mcrl2" ; "11073.mcrl2")]

#[test_case(include_str!("../../../examples/mCRL2/industrial/lift/lift3-final.mcrl2"), "tests/snapshot/result_lift3-final.mcrl2" ; "lift3-final.mcrl2")]

#[test_case(include_str!("../../../examples/mCRL2/industrial/lift/lift3-init.mcrl2"), "tests/snapshot/result_lift3-init.mcrl2" ; "lift3-init.mcrl2")]

#[test_case(include_str!("../../../examples/mCRL2/language/delta.mcrl2"), "tests/snapshot/result_delta.mcrl2" ; "delta.mcrl2")]

#[test_case(include_str!("../../../examples/mCRL2/language/delta0.mcrl2"), "tests/snapshot/result_delta0.mcrl2" ; "delta0.mcrl2")]

#[test_case(include_str!("../../../examples/mCRL2/language/divide2_10.mcrl2"), "tests/snapshot/result_divide2_10.mcrl2" ; "divide2_10.mcrl2")]

#[test_case(include_str!("../../../examples/mCRL2/language/divide2_100.mcrl2"), "tests/snapshot/result_divide2_100.mcrl2" ; "divide2_100.mcrl2")]

#[test_case(include_str!("../../../examples/mCRL2/language/divide2_500.mcrl2"), "tests/snapshot/result_divide2_500.mcrl2" ; "divide2_500.mcrl2")]

#[test_case(include_str!("../../../examples/mCRL2/language/exists.mcrl2"), "tests/snapshot/result_exists.mcrl2" ; "exists.mcrl2")]

#[test_case(include_str!("../../../examples/mCRL2/language/forall.mcrl2"), "tests/snapshot/result_forall.mcrl2" ; "forall.mcrl2")]

#[test_case(include_str!("../../../examples/mCRL2/language/funccomp.mcrl2"), "tests/snapshot/result_funccomp.mcrl2" ; "funccomp.mcrl2")]

#[test_case(include_str!("../../../examples/mCRL2/language/gpa_10_1.mcrl2"), "tests/snapshot/result_gpa_10_1.mcrl2" ; "gpa_10_1.mcrl2")]

#[test_case(include_str!("../../../examples/mCRL2/language/gpa_10_2.mcrl2"), "tests/snapshot/result_gpa_10_2.mcrl2" ; "gpa_10_2.mcrl2")]

#[test_case(include_str!("../../../examples/mCRL2/language/gpa_10_3.mcrl2"), "tests/snapshot/result_gpa_10_3.mcrl2" ; "gpa_10_3.mcrl2")]

#[test_case(include_str!("../../../examples/mCRL2/language/lambda.mcrl2"), "tests/snapshot/result_lambda.mcrl2" ; "lambda.mcrl2")]

#[test_case(include_str!("../../../examples/mCRL2/language/list.mcrl2"), "tests/snapshot/result_list.mcrl2" ; "list.mcrl2")]

#[test_case(include_str!("../../../examples/mCRL2/language/numbers.mcrl2"), "tests/snapshot/result_numbers.mcrl2" ; "numbers.mcrl2")]

#[test_case(include_str!("../../../examples/mCRL2/language/rational.mcrl2"), "tests/snapshot/result_rational.mcrl2" ; "rational.mcrl2")]

#[test_case(include_str!("../../../examples/mCRL2/language/sets_bags.mcrl2"), "tests/snapshot/result_sets_bags.mcrl2" ; "sets_bags.mcrl2")]

#[test_case(include_str!("../../../examples/mCRL2/language/small1.mcrl2"), "tests/snapshot/result_small1.mcrl2" ; "small1.mcrl2")]

#[test_case(include_str!("../../../examples/mCRL2/language/small2.mcrl2"), "tests/snapshot/result_small2.mcrl2" ; "small2.mcrl2")]

#[test_case(include_str!("../../../examples/mCRL2/language/small3.mcrl2"), "tests/snapshot/result_small3.mcrl2" ; "small3.mcrl2")]

#[test_case(include_str!("../../../examples/mCRL2/language/struct.mcrl2"), "tests/snapshot/result_struct.mcrl2" ; "struct.mcrl2")]

#[test_case(include_str!("../../../examples/mCRL2/language/tau.mcrl2"), "tests/snapshot/result_tau.mcrl2" ; "tau.mcrl2")]

#[test_case(include_str!("../../../examples/mCRL2/language/time.mcrl2"), "tests/snapshot/result_time.mcrl2" ; "time.mcrl2")]

#[test_case(include_str!("../../../examples/mCRL2/language/upcast.mcrl2"), "tests/snapshot/result_upcast.mcrl2" ; "upcast.mcrl2")]

#[test_case(include_str!("../../../examples/mCRL2/probabilistic/airplane_ticket/airplane_ticket.mcrl2"), "tests/snapshot/result_airplane_ticket.mcrl2" ; "airplane_ticket.mcrl2")]

#[test_case(include_str!("../../../examples/mCRL2/probabilistic/ant_on_grid/ant_on_grid.mcrl2"), "tests/snapshot/result_ant_on_grid.mcrl2" ; "ant_on_grid.mcrl2")]

#[test_case(include_str!("../../../examples/mCRL2/probabilistic/coin_tossing/coins.mcrl2"), "tests/snapshot/result_coins.mcrl2" ; "coins.mcrl2")]

#[test_case(include_str!("../../../examples/mCRL2/probabilistic/coins_simulate_dice/dice.mcrl2"), "tests/snapshot/result_dice.mcrl2" ; "dice.mcrl2")]

#[test_case(include_str!("../../../examples/mCRL2/probabilistic/game_of_goose/game_of_goose_stochastic.mcrl2"), "tests/snapshot/result_game_of_goose_stochastic.mcrl2" ; "game_of_goose_stochastic.mcrl2")]

#[test_case(include_str!("../../../examples/mCRL2/probabilistic/monty_hall_tv_show/monty_hall.mcrl2"), "tests/snapshot/result_monty_hall.mcrl2" ; "monty_hall.mcrl2")]

#[test_case(include_str!("../../../examples/mCRL2/probabilistic/self_stabilisation/self_stabilisation.mcrl2"), "tests/snapshot/result_self_stabilisation.mcrl2" ; "self_stabilisation.mcrl2")]

#[test_case(include_str!("../../../examples/mCRL2/probabilistic/shared_coin_protocol/shared_coin_protocol.mcrl2"), "tests/snapshot/result_shared_coin_protocol.mcrl2" ; "shared_coin_protocol.mcrl2")]

#[test_case(include_str!("../../../examples/mCRL2/probabilistic/slot_machines/1slot/1slot_spec.mcrl2"), "tests/snapshot/result_1slot_spec.mcrl2" ; "1slot_spec.mcrl2")]

#[test_case(include_str!("../../../examples/mCRL2/probabilistic/slot_machines/3slot/3slot_spec.mcrl2"), "tests/snapshot/result_3slot_spec.mcrl2" ; "3slot_spec.mcrl2")]

#[test_case(include_str!("../../../examples/mCRL2/probabilistic/slot_machines/3slot_hold/3slot_hold_spec.mcrl2"), "tests/snapshot/result_3slot_hold_spec.mcrl2" ; "3slot_hold_spec.mcrl2")]

#[test_case(include_str!("../../../examples/mCRL2/probabilistic/slot_machines/3slot_hold/3slot_hold_spec_average.mcrl2"), "tests/snapshot/result_3slot_hold_spec_average.mcrl2" ; "3slot_hold_spec_average.mcrl2")]

#[test_case(include_str!("../../../examples/mCRL2/probabilistic/slot_machines/paylines/10_paylines_game_spec.mcrl2"), "tests/snapshot/result_10_paylines_game_spec.mcrl2" ; "10_paylines_game_spec.mcrl2")]

#[test_case(include_str!("../../../examples/mCRL2/probabilistic/slot_machines/paylines/5_paylines_game_spec.mcrl2"), "tests/snapshot/result_5_paylines_game_spec.mcrl2" ; "5_paylines_game_spec.mcrl2")]

#[test_case(include_str!("../../../examples/mCRL2/probabilistic/slot_machines/reels_game/reels_game_spec.mcrl2"), "tests/snapshot/result_reels_game_spec.mcrl2" ; "reels_game_spec.mcrl2")]

#[test_case(include_str!("../../../examples/mCRL2/probabilistic/spinning_mule_woolhouse/spinning_mule.mcrl2"), "tests/snapshot/result_spinning_mule.mcrl2" ; "spinning_mule.mcrl2")]

#[test_case(include_str!("../../../examples/mCRL2/probabilistic/spinning_mule_woolhouse/spinning_mule_optimized.mcrl2"), "tests/snapshot/result_spinning_mule_optimized.mcrl2" ; "spinning_mule_optimized.mcrl2")]

#[test_case(include_str!("../../../examples/mCRL2/probabilistic/spinning_mule_woolhouse/spinning_mule_woolhouse.mcrl2"), "tests/snapshot/result_spinning_mule_woolhouse.mcrl2" ; "spinning_mule_woolhouse.mcrl2")]

#[test_case(include_str!("../../../examples/mCRL2/probabilistic/sultan_of_persia/sultan_of_persia.mcrl2"), "tests/snapshot/result_sultan_of_persia.mcrl2" ; "sultan_of_persia.mcrl2")]

#[test_case(include_str!("../../../examples/mCRL2/project/wafer_stepper/wafer_stepper.mcrl2"), "tests/snapshot/result_wafer_stepper.mcrl2" ; "wafer_stepper.mcrl2")]

#[test_case(include_str!("../../../examples/mCRL2/software_models/Knuths_dancing_links/Dancing_links/Dancing_links_spec.mcrl2"), "tests/snapshot/result_dancing_links_spec.mcrl2" ; "dancing_links_spec.mcrl2")]

#[test_case(include_str!("../../../examples/mCRL2/software_models/Knuths_dancing_links/Dancing_links_no_stack/Dancing_links_no_stack_spec.mcrl2"), "tests/snapshot/result_dancing_links_no_stack_spec.mcrl2" ; "dancing_links_no_stack_spec.mcrl2")]

#[test_case(include_str!("../../../examples/mCRL2/software_models/Knuths_dancing_links/Dancing_links_remove_0/Dancing_links_remove_0_spec.mcrl2"), "tests/snapshot/result_dancing_links_remove_0_spec.mcrl2" ; "dancing_links_remove_0_spec.mcrl2")]

#[test_case(include_str!("../../../examples/mCRL2/software_models/Lamport_queue/Lamport_queue_spec.mcrl2"), "tests/snapshot/result_lamport_queue_spec.mcrl2" ; "lamport_queue_spec.mcrl2")]

#[test_case(include_str!("../../../examples/mCRL2/software_models/Petersons_mutex/Petersons_F_F/Petersons_F_F_spec.mcrl2"), "tests/snapshot/result_petersons_f_f_spec.mcrl2" ; "petersons_f_f_spec.mcrl2")]

#[test_case(include_str!("../../../examples/mCRL2/software_models/Petersons_mutex/Petersons_F_T/Petersons_F_T_spec.mcrl2"), "tests/snapshot/result_petersons_f_t_spec.mcrl2" ; "petersons_f_t_spec.mcrl2")]

#[test_case(include_str!("../../../examples/mCRL2/software_models/Petersons_mutex/Petersons_T_T/Petersons_T_T_spec.mcrl2"), "tests/snapshot/result_petersons_t_t_spec.mcrl2" ; "petersons_t_t_spec.mcrl2")]

#[test_case(include_str!("../../../examples/mCRL2/software_models/Treiber_stack/Treiber_CAS/Treiber_CAS_spec.mcrl2"), "tests/snapshot/result_treiber_cas_spec.mcrl2" ; "treiber_cas_spec.mcrl2")]

#[test_case(include_str!("../../../examples/mCRL2/software_models/Treiber_stack/Treiber_DCAS/Treiber_DCAS_spec.mcrl2"), "tests/snapshot/result_treiber_dcas_spec.mcrl2" ; "treiber_dcas_spec.mcrl2")]

#[test_case(include_str!("../../../examples/mCRL2/software_models/Treiber_stack/Treiber_no_CAS/Treiber_no_CAS_spec.mcrl2"), "tests/snapshot/result_treiber_no_cas_spec.mcrl2" ; "treiber_no_cas_spec.mcrl2")]

#[test_case(include_str!("../../../examples/mCRL2/timed/ball_game/ball_game.mcrl2"), "tests/snapshot/result_ball_game.mcrl2" ; "ball_game.mcrl2")]

#[test_case(include_str!("../../../examples/mCRL2/timed/clock/clock_drift.mcrl2"), "tests/snapshot/result_clock_drift.mcrl2" ; "clock_drift.mcrl2")]

#[test_case(include_str!("../../../examples/mCRL2/timed/clock/clock_exact.mcrl2"), "tests/snapshot/result_clock_exact.mcrl2" ; "clock_exact.mcrl2")]

#[test_case(include_str!("../../../examples/mCRL2/timed/clock/clock_hasty.mcrl2"), "tests/snapshot/result_clock_hasty.mcrl2" ; "clock_hasty.mcrl2")]

#[test_case(include_str!("../../../examples/mCRL2/timed/fischer/fischer.mcrl2"), "tests/snapshot/result_fischer.mcrl2" ; "fischer.mcrl2")]

#[test_case(include_str!("../../../examples/mCRL2/timed/light/light.mcrl2"), "tests/snapshot/result_light.mcrl2" ; "light.mcrl2")]

#[test_case(include_str!("../../../examples/mCRL2/timed/simple/simple.mcrl2"), "tests/snapshot/result_simple.mcrl2" ; "simple.mcrl2")]

#[test_case(include_str!("../../../examples/mCRL2/visualisation/carpet/carpet.mcrl2"), "tests/snapshot/result_carpet.mcrl2" ; "carpet.mcrl2")]

#[test_case(include_str!("../../../examples/mCRL2/visualisation/cube/cube.mcrl2"), "tests/snapshot/result_cube.mcrl2" ; "cube.mcrl2")]

    }

#[cfg_attr(miri, ignore)]

#[test_case(include_str!("../../../examples/mCRL2/academic/abp/infinitely_often_enabled_then_infinitely_often_taken.mcf"), "tests/snapshot/result_infinitely_often_enabled_then_infinitely_often_taken.mcf" ; "infinitely_often_enabled_then_infinitely_often_taken.mcf")]

#[test_case(include_str!("../../../examples/mCRL2/academic/abp/infinitely_often_lost.mcf"), "tests/snapshot/result_infinitely_often_lost.mcf" ; "infinitely_often_lost.mcf")]

#[test_case(include_str!("../../../examples/mCRL2/academic/abp/infinitely_often_receive_d1.mcf"), "tests/snapshot/result_infinitely_often_receive_d1.mcf" ; "infinitely_often_receive_d1.mcf")]

#[test_case(include_str!("../../../examples/mCRL2/academic/abp/infinitely_often_receive_for_all_d.mcf"), "tests/snapshot/result_infinitely_often_receive_for_all_d.mcf" ; "infinitely_often_receive_for_all_d.mcf")]

#[test_case(include_str!("../../../examples/mCRL2/academic/abp/no_duplication_of_messages.mcf"), "tests/snapshot/result_no_duplication_of_messages.mcf" ; "no_duplication_of_messages.mcf")]

#[test_case(include_str!("../../../examples/mCRL2/academic/abp/no_generation_of_messages.mcf"), "tests/snapshot/result_no_generation_of_messages.mcf" ; "no_generation_of_messages.mcf")]

#[test_case(include_str!("../../../examples/mCRL2/academic/abp/nodeadlock.mcf"), "tests/snapshot/result_nodeadlock.mcf" ; "nodeadlock.mcf")]

#[test_case(include_str!("../../../examples/mCRL2/academic/abp/read_then_eventually_send.mcf"), "tests/snapshot/result_read_then_eventually_send.mcf" ; "read_then_eventually_send.mcf")]

#[test_case(include_str!("../../../examples/mCRL2/academic/abp/read_then_eventually_send_if_fair.mcf"), "tests/snapshot/result_read_then_eventually_send_if_fair.mcf" ; "read_then_eventually_send_if_fair.mcf")]

#[test_case(include_str!("../../../examples/mCRL2/academic/bakery/always_can_get_number.mcf"), "tests/snapshot/result_always_can_get_number.mcf" ; "always_can_get_number.mcf")]

#[test_case(include_str!("../../../examples/mCRL2/academic/bakery/get_at_least_number_circulating.mcf"), "tests/snapshot/result_get_at_least_number_circulating.mcf" ; "get_at_least_number_circulating.mcf")]

#[test_case(include_str!("../../../examples/mCRL2/academic/bakery/mutual_exclusion.mcf"), "tests/snapshot/result_mutual_exclusion.mcf" ; "mutual_exclusion.mcf")]

#[test_case(include_str!("../../../examples/mCRL2/academic/bakery/request_can_eventually_enter.mcf"), "tests/snapshot/result_request_can_eventually_enter.mcf" ; "request_can_eventually_enter.mcf")]

#[test_case(include_str!("../../../examples/mCRL2/academic/bakery/request_must_eventually_enter.mcf"), "tests/snapshot/result_request_must_eventually_enter.mcf" ; "request_must_eventually_enter.mcf")]

#[test_case(include_str!("../../../examples/mCRL2/academic/bke/secret_not_leaked.mcf"), "tests/snapshot/result_secret_not_leaked.mcf" ; "secret_not_leaked.mcf")]

#[test_case(include_str!("../../../examples/mCRL2/academic/bounded_ricart-agrawala/RA_fixed/properties/deadlock freedom.mcf"), "tests/snapshot/result_deadlock_freedom.mcf" ; "deadlock_freedom.mcf")]

#[test_case(include_str!("../../../examples/mCRL2/academic/bounded_ricart-agrawala/RA_fixed/properties/no deadlock in model.mcf"), "tests/snapshot/result_no_deadlock_in_model.mcf" ; "no_deadlock_in_model.mcf")]

#[test_case(include_str!("../../../examples/mCRL2/academic/bounded_ricart-agrawala/RA_fixed/properties/starvation freedom.mcf"), "tests/snapshot/result_starvation_freedom.mcf" ; "starvation_freedom.mcf")]

#[test_case(include_str!("../../../examples/mCRL2/academic/dining/nostarvation.mcf"), "tests/snapshot/result_nostarvation.mcf" ; "nostarvation.mcf")]

#[test_case(include_str!("../../../examples/mCRL2/academic/dining/nostuffing.mcf"), "tests/snapshot/result_nostuffing.mcf" ; "nostuffing.mcf")]

#[test_case(include_str!("../../../examples/mCRL2/academic/food_distribution/sustained_delivery.mcf"), "tests/snapshot/result_sustained_delivery.mcf" ; "sustained_delivery.mcf")]

#[test_case(include_str!("../../../examples/mCRL2/academic/leader/at_most_one_leader.mcf"), "tests/snapshot/result_at_most_one_leader.mcf" ; "at_most_one_leader.mcf")]

#[test_case(include_str!("../../../examples/mCRL2/academic/leader/leader_always_elected.mcf"), "tests/snapshot/result_leader_always_elected.mcf" ; "leader_always_elected.mcf")]

#[test_case(include_str!("../../../examples/mCRL2/academic/minepump_product_line/family_based_experiments/formula1/prop1.mcf"), "tests/snapshot/result_prop1.mcf" ; "prop1.mcf")]

#[test_case(include_str!("../../../examples/mCRL2/academic/minepump_product_line/family_based_experiments/formula10/prop10.mcf"), "tests/snapshot/result_prop10.mcf" ; "prop10.mcf")]

#[test_case(include_str!("../../../examples/mCRL2/academic/minepump_product_line/family_based_experiments/formula11/prop11.mcf"), "tests/snapshot/result_prop11.mcf" ; "prop11.mcf")]

#[test_case(include_str!("../../../examples/mCRL2/academic/minepump_product_line/family_based_experiments/formula12/prop12.mcf"), "tests/snapshot/result_prop12.mcf" ; "prop12.mcf")]

#[test_case(include_str!("../../../examples/mCRL2/academic/minepump_product_line/family_based_experiments/formula2/prop2.mcf"), "tests/snapshot/result_prop2.mcf" ; "prop2.mcf")]

#[test_case(include_str!("../../../examples/mCRL2/academic/minepump_product_line/family_based_experiments/formula3/prop3.mcf"), "tests/snapshot/result_prop3.mcf" ; "prop3.mcf")]

#[test_case(include_str!("../../../examples/mCRL2/academic/minepump_product_line/family_based_experiments/formula4/prop4.mcf"), "tests/snapshot/result_prop4.mcf" ; "prop4.mcf")]

#[test_case(include_str!("../../../examples/mCRL2/academic/minepump_product_line/family_based_experiments/formula5/prop5.mcf"), "tests/snapshot/result_prop5.mcf" ; "prop5.mcf")]

#[test_case(include_str!("../../../examples/mCRL2/academic/minepump_product_line/family_based_experiments/formula6/prop6.mcf"), "tests/snapshot/result_prop6.mcf" ; "prop6.mcf")]

#[test_case(include_str!("../../../examples/mCRL2/academic/minepump_product_line/family_based_experiments/formula7/prop7.mcf"), "tests/snapshot/result_prop7.mcf" ; "prop7.mcf")]

#[test_case(include_str!("../../../examples/mCRL2/academic/minepump_product_line/family_based_experiments/formula8/prop8.mcf"), "tests/snapshot/result_prop8.mcf" ; "prop8.mcf")]

#[test_case(include_str!("../../../examples/mCRL2/academic/minepump_product_line/family_based_experiments/formula9/prop9.mcf"), "tests/snapshot/result_prop9.mcf" ; "prop9.mcf")]

#[test_case(include_str!("../../../examples/mCRL2/academic/mpsu/mpsu1.mcf"), "tests/snapshot/result_mpsu1.mcf" ; "mpsu1.mcf")]

#[test_case(include_str!("../../../examples/mCRL2/academic/mpsu/mpsu2.mcf"), "tests/snapshot/result_mpsu2.mcf" ; "mpsu2.mcf")]

#[test_case(include_str!("../../../examples/mCRL2/academic/mpsu/mpsu3.mcf"), "tests/snapshot/result_mpsu3.mcf" ; "mpsu3.mcf")]

#[test_case(include_str!("../../../examples/mCRL2/academic/mpsu/mpsu4.mcf"), "tests/snapshot/result_mpsu4.mcf" ; "mpsu4.mcf")]

#[test_case(include_str!("../../../examples/mCRL2/academic/mpsu/mpsu5.mcf"), "tests/snapshot/result_mpsu5.mcf" ; "mpsu5.mcf")]

#[test_case(include_str!("../../../examples/mCRL2/academic/mpsu/mpsu6.mcf"), "tests/snapshot/result_mpsu6.mcf" ; "mpsu6.mcf")]

#[test_case(include_str!("../../../examples/mCRL2/academic/mutex_models/Dekker/properties/Always eventually request.mcf"), "tests/snapshot/result_always_eventually_request.mcf" ; "always_eventually_request.mcf")]

#[test_case(include_str!("../../../examples/mCRL2/academic/mutex_models/Dekker/properties/Eventual access if fair.mcf"), "tests/snapshot/result_eventual_access_if_fair.mcf" ; "eventual_access_if_fair.mcf")]

#[test_case(include_str!("../../../examples/mCRL2/academic/mutex_models/Dekker/properties/Eventual access.mcf"), "tests/snapshot/result_eventual_access.mcf" ; "eventual_access.mcf")]

#[test_case(include_str!("../../../examples/mCRL2/academic/mutex_models/Petersons/properties/Bounded overtaking.mcf"), "tests/snapshot/result_bounded_overtaking.mcf" ; "bounded_overtaking.mcf")]

#[test_case(include_str!("../../../examples/mCRL2/academic/mutex_models/Petersons/properties/Eventual access without cooperation.mcf"), "tests/snapshot/result_eventual_access_without_cooperation.mcf" ; "eventual_access_without_cooperation.mcf")]

#[test_case(include_str!("../../../examples/mCRL2/academic/non-atomic_registers/Aravind_BLRU/properties/No deadlock.mcf"), "tests/snapshot/result_no_deadlock.mcf" ; "no_deadlock.mcf")]

#[test_case(include_str!("../../../examples/mCRL2/academic/non-atomic_registers/Aravind_BLRU/properties/Reachable.mcf"), "tests/snapshot/result_reachable.mcf" ; "reachable.mcf")]

#[test_case(include_str!("../../../examples/mCRL2/academic/onebit/infinitely_often_receive_dat1.mcf"), "tests/snapshot/result_infinitely_often_receive_dat1.mcf" ; "infinitely_often_receive_dat1.mcf")]

#[test_case(include_str!("../../../examples/mCRL2/academic/parallel_proc_with_global_var/parallel_counting.mcf"), "tests/snapshot/result_parallel_counting.mcf" ; "parallel_counting.mcf")]

#[test_case(include_str!("../../../examples/mCRL2/academic/peterson_justness/justlive.mcf"), "tests/snapshot/result_justlive.mcf" ; "justlive.mcf")]

#[test_case(include_str!("../../../examples/mCRL2/academic/scheduler/infinitely_often_enabled_then_infinitely_often_taken_a.mcf"), "tests/snapshot/result_infinitely_often_enabled_then_infinitely_often_taken_a.mcf" ; "infinitely_often_enabled_then_infinitely_often_taken_a.mcf")]

#[test_case(include_str!("../../../examples/mCRL2/academic/trains/infinitely_often_enabled_then_infinitely_often_taken_enter.mcf"), "tests/snapshot/result_infinitely_often_enabled_then_infinitely_often_taken_enter.mcf" ; "infinitely_often_enabled_then_infinitely_often_taken_enter.mcf")]

#[test_case(include_str!("../../../examples/mCRL2/games/beggar_my_neighbour/exists_an_infinite_game.mcf"), "tests/snapshot/result_exists_an_infinite_game.mcf" ; "exists_an_infinite_game.mcf")]

#[test_case(include_str!("../../../examples/mCRL2/games/domineering/eventually_player1_or_player2_wins.mcf"), "tests/snapshot/result_eventually_player1_or_player2_wins.mcf" ; "eventually_player1_or_player2_wins.mcf")]

#[test_case(include_str!("../../../examples/mCRL2/games/domineering/player1_can_win.mcf"), "tests/snapshot/result_player1_can_win.mcf" ; "player1_can_win.mcf")]

#[test_case(include_str!("../../../examples/mCRL2/games/domineering/player2_can_win.mcf"), "tests/snapshot/result_player2_can_win.mcf" ; "player2_can_win.mcf")]

#[test_case(include_str!("../../../examples/mCRL2/games/four_in_a_row/red_wins.mcf"), "tests/snapshot/result_red_wins.mcf" ; "red_wins.mcf")]

#[test_case(include_str!("../../../examples/mCRL2/games/open_field_tic_tac_toe/red_has_a_winning_strategy.mcf"), "tests/snapshot/result_red_has_a_winning_strategy.mcf" ; "red_has_a_winning_strategy.mcf")]

#[test_case(include_str!("../../../examples/mCRL2/games/open_field_tic_tac_toe/yellow_has_a_winning_strategy.mcf"), "tests/snapshot/result_yellow_has_a_winning_strategy.mcf" ; "yellow_has_a_winning_strategy.mcf")]

#[test_case(include_str!("../../../examples/mCRL2/games/othello/exists_draw.mcf"), "tests/snapshot/result_exists_draw.mcf" ; "exists_draw.mcf")]

#[test_case(include_str!("../../../examples/mCRL2/games/othello/red_can_win.mcf"), "tests/snapshot/result_red_can_win.mcf" ; "red_can_win.mcf")]

#[test_case(include_str!("../../../examples/mCRL2/games/othello/red_wins_always.mcf"), "tests/snapshot/result_red_wins_always.mcf" ; "red_wins_always.mcf")]

#[test_case(include_str!("../../../examples/mCRL2/games/othello/white_can_win.mcf"), "tests/snapshot/result_white_can_win.mcf" ; "white_can_win.mcf")]

#[test_case(include_str!("../../../examples/mCRL2/games/othello/white_wins_always.mcf"), "tests/snapshot/result_white_wins_always.mcf" ; "white_wins_always.mcf")]

#[test_case(include_str!("../../../examples/mCRL2/games/quoridor/properties/rule1.mcf"), "tests/snapshot/result_rule1.mcf" ; "rule1.mcf")]

#[test_case(include_str!("../../../examples/mCRL2/games/quoridor/properties/rule11.mcf"), "tests/snapshot/result_rule11.mcf" ; "rule11.mcf")]

#[test_case(include_str!("../../../examples/mCRL2/games/quoridor/properties/rule12.mcf"), "tests/snapshot/result_rule12.mcf" ; "rule12.mcf")]

#[test_case(include_str!("../../../examples/mCRL2/games/quoridor/properties/rule14.mcf"), "tests/snapshot/result_rule14.mcf" ; "rule14.mcf")]

#[test_case(include_str!("../../../examples/mCRL2/games/quoridor/properties/rule15.mcf"), "tests/snapshot/result_rule15.mcf" ; "rule15.mcf")]

#[test_case(include_str!("../../../examples/mCRL2/games/quoridor/properties/rule3.mcf"), "tests/snapshot/result_rule3.mcf" ; "rule3.mcf")]

#[test_case(include_str!("../../../examples/mCRL2/games/quoridor/properties/rule4.mcf"), "tests/snapshot/result_rule4.mcf" ; "rule4.mcf")]

#[test_case(include_str!("../../../examples/mCRL2/games/quoridor/properties/rule5.mcf"), "tests/snapshot/result_rule5.mcf" ; "rule5.mcf")]

#[test_case(include_str!("../../../examples/mCRL2/games/quoridor/properties/rule6a.mcf"), "tests/snapshot/result_rule6a.mcf" ; "rule6a.mcf")]

#[test_case(include_str!("../../../examples/mCRL2/games/quoridor/properties/rule6b.mcf"), "tests/snapshot/result_rule6b.mcf" ; "rule6b.mcf")]

#[test_case(include_str!("../../../examples/mCRL2/games/quoridor/properties/rule789.mcf"), "tests/snapshot/result_rule789.mcf" ; "rule789.mcf")]

#[test_case(include_str!("../../../examples/mCRL2/games/quoridor/properties/winning_strategy_player_1.mcf"), "tests/snapshot/result_winning_strategy_player_1.mcf" ; "winning_strategy_player_1.mcf")]

#[test_case(include_str!("../../../examples/mCRL2/games/quoridor/properties/winning_strategy_player_2.mcf"), "tests/snapshot/result_winning_strategy_player_2.mcf" ; "winning_strategy_player_2.mcf")]

#[test_case(include_str!("../../../examples/mCRL2/games/snake/black_can_win.mcf"), "tests/snapshot/result_black_can_win.mcf" ; "black_can_win.mcf")]

#[test_case(include_str!("../../../examples/mCRL2/games/snake/black_has_winning_strategy.mcf"), "tests/snapshot/result_black_has_winning_strategy.mcf" ; "black_has_winning_strategy.mcf")]

#[test_case(include_str!("../../../examples/mCRL2/games/snake/eventually_white_or_black_wins.mcf"), "tests/snapshot/result_eventually_white_or_black_wins.mcf" ; "eventually_white_or_black_wins.mcf")]

#[test_case(include_str!("../../../examples/mCRL2/games/snake/white_has_winning_strategy.mcf"), "tests/snapshot/result_white_has_winning_strategy.mcf" ; "white_has_winning_strategy.mcf")]

#[test_case(include_str!("../../../examples/mCRL2/games/tictactoe/has_player_cross_a_winning_strategy.mcf"), "tests/snapshot/result_has_player_cross_a_winning_strategy.mcf" ; "has_player_cross_a_winning_strategy.mcf")]

#[test_case(include_str!("../../../examples/mCRL2/games/tictactoe/one_wrong_move.mcf"), "tests/snapshot/result_one_wrong_move.mcf" ; "one_wrong_move.mcf")]

#[test_case(include_str!("../../../examples/mCRL2/industrial/DIRAC/properties_SMS/eventuallyDeleted.mcf"), "tests/snapshot/result_eventuallydeleted.mcf" ; "eventuallydeleted.mcf")]

#[test_case(include_str!("../../../examples/mCRL2/industrial/DIRAC/properties_SMS/noTransitFromDeleted.mcf"), "tests/snapshot/result_notransitfromdeleted.mcf" ; "notransitfromdeleted.mcf")]

#[test_case(include_str!("../../../examples/mCRL2/industrial/DIRAC/properties_WMS/jobFailedToDone.mcf"), "tests/snapshot/result_jobfailedtodone.mcf" ; "jobfailedtodone.mcf")]

#[test_case(include_str!("../../../examples/mCRL2/industrial/DIRAC/properties_WMS/noZombieJobs.mcf"), "tests/snapshot/result_nozombiejobs.mcf" ; "nozombiejobs.mcf")]

#[test_case(include_str!("../../../examples/mCRL2/industrial/ERTMS/version1A/section_I/IU/deterministic_stabilisation.mcf"), "tests/snapshot/result_deterministic_stabilisation.mcf" ; "deterministic_stabilisation.mcf")]

#[test_case(include_str!("../../../examples/mCRL2/industrial/ERTMS/version1A/section_I/IU/no_collision.mcf"), "tests/snapshot/result_no_collision.mcf" ; "no_collision.mcf")]

#[test_case(include_str!("../../../examples/mCRL2/industrial/ERTMS/version1A/section_I/IU/strong_determinacy.mcf"), "tests/snapshot/result_strong_determinacy.mcf" ; "strong_determinacy.mcf")]

#[test_case(include_str!("../../../examples/mCRL2/industrial/ERTMS/version1A/section_I/IU/termination.mcf"), "tests/snapshot/result_termination.mcf" ; "termination.mcf")]

#[test_case(include_str!("../../../examples/mCRL2/industrial/MLV/properties/CONT.1.3.mcf"), "tests/snapshot/result_cont.1.3.mcf" ; "cont.1.3.mcf")]

#[test_case(include_str!("../../../examples/mCRL2/industrial/MLV/properties/CONT.38.mcf"), "tests/snapshot/result_cont.38.mcf" ; "cont.38.mcf")]

#[test_case(include_str!("../../../examples/mCRL2/industrial/MLV/properties/CONT_1.mcf"), "tests/snapshot/result_cont_1.mcf" ; "cont_1.mcf")]

#[test_case(include_str!("../../../examples/mCRL2/industrial/MLV/properties/CONT_10.mcf"), "tests/snapshot/result_cont_10.mcf" ; "cont_10.mcf")]

#[test_case(include_str!("../../../examples/mCRL2/industrial/MLV/properties/CONT_13.mcf"), "tests/snapshot/result_cont_13.mcf" ; "cont_13.mcf")]

#[test_case(include_str!("../../../examples/mCRL2/industrial/MLV/properties/CONT_15.mcf"), "tests/snapshot/result_cont_15.mcf" ; "cont_15.mcf")]

#[test_case(include_str!("../../../examples/mCRL2/industrial/MLV/properties/CONT_19.mcf"), "tests/snapshot/result_cont_19.mcf" ; "cont_19.mcf")]

#[test_case(include_str!("../../../examples/mCRL2/industrial/MLV/properties/CONT_21.mcf"), "tests/snapshot/result_cont_21.mcf" ; "cont_21.mcf")]

#[test_case(include_str!("../../../examples/mCRL2/industrial/MLV/properties/CONT_25.mcf"), "tests/snapshot/result_cont_25.mcf" ; "cont_25.mcf")]

#[test_case(include_str!("../../../examples/mCRL2/industrial/MLV/properties/CONT_3.mcf"), "tests/snapshot/result_cont_3.mcf" ; "cont_3.mcf")]

#[test_case(include_str!("../../../examples/mCRL2/industrial/MLV/properties/CONT_46.mcf"), "tests/snapshot/result_cont_46.mcf" ; "cont_46.mcf")]

#[test_case(include_str!("../../../examples/mCRL2/industrial/MLV/properties/CONT_4_1.mcf"), "tests/snapshot/result_cont_4_1.mcf" ; "cont_4_1.mcf")]

#[test_case(include_str!("../../../examples/mCRL2/industrial/MLV/properties/CONT_4_2.mcf"), "tests/snapshot/result_cont_4_2.mcf" ; "cont_4_2.mcf")]

#[test_case(include_str!("../../../examples/mCRL2/industrial/MLV/properties/CONT_5.mcf"), "tests/snapshot/result_cont_5.mcf" ; "cont_5.mcf")]

#[test_case(include_str!("../../../examples/mCRL2/industrial/MLV/properties/CONT_6.mcf"), "tests/snapshot/result_cont_6.mcf" ; "cont_6.mcf")]

#[test_case(include_str!("../../../examples/mCRL2/industrial/MLV/properties/CONT_7.mcf"), "tests/snapshot/result_cont_7.mcf" ; "cont_7.mcf")]

#[test_case(include_str!("../../../examples/mCRL2/industrial/MLV/properties/CONT_8.mcf"), "tests/snapshot/result_cont_8.mcf" ; "cont_8.mcf")]

#[test_case(include_str!("../../../examples/mCRL2/industrial/MLV/properties/CONT_9.mcf"), "tests/snapshot/result_cont_9.mcf" ; "cont_9.mcf")]

#[test_case(include_str!("../../../examples/mCRL2/industrial/MLV/properties/SAV.1.mcf"), "tests/snapshot/result_sav.1.mcf" ; "sav.1.mcf")]

#[test_case(include_str!("../../../examples/mCRL2/industrial/MLV/properties/SAV.16.mcf"), "tests/snapshot/result_sav.16.mcf" ; "sav.16.mcf")]

#[test_case(include_str!("../../../examples/mCRL2/industrial/MLV/properties/SAV.17.mcf"), "tests/snapshot/result_sav.17.mcf" ; "sav.17.mcf")]

#[test_case(include_str!("../../../examples/mCRL2/industrial/MLV/properties/SAV.22.mcf"), "tests/snapshot/result_sav.22.mcf" ; "sav.22.mcf")]

#[test_case(include_str!("../../../examples/mCRL2/industrial/MLV/properties/Scenario_Error_in_selftest.mcf"), "tests/snapshot/result_scenario_error_in_selftest.mcf" ; "scenario_error_in_selftest.mcf")]

#[test_case(include_str!("../../../examples/mCRL2/industrial/MLV/properties/Scenario_New_patient.mcf"), "tests/snapshot/result_scenario_new_patient.mcf" ; "scenario_new_patient.mcf")]

#[test_case(include_str!("../../../examples/mCRL2/industrial/MLV/properties/Scenario_Resume_ventilation.mcf"), "tests/snapshot/result_scenario_resume_ventilation.mcf" ; "scenario_resume_ventilation.mcf")]

#[test_case(include_str!("../../../examples/mCRL2/industrial/flexray/mucalc/eventually_comm.mcf"), "tests/snapshot/result_eventually_comm.mcf" ; "eventually_comm.mcf")]

#[test_case(include_str!("../../../examples/mCRL2/industrial/flexray/mucalc/eventually_startup.mcf"), "tests/snapshot/result_eventually_startup.mcf" ; "eventually_startup.mcf")]

#[test_case(include_str!("../../../examples/mCRL2/industrial/ieee-11073/data_can_be_communicated.mcf"), "tests/snapshot/result_data_can_be_communicated.mcf" ; "data_can_be_communicated.mcf")]

#[test_case(include_str!("../../../examples/mCRL2/industrial/ieee-11073/infinite_data_communication_is_possible.mcf"), "tests/snapshot/result_infinite_data_communication_is_possible.mcf" ; "infinite_data_communication_is_possible.mcf")]

#[test_case(include_str!("../../../examples/mCRL2/industrial/ieee-11073/no_inconsistent_operating_states.mcf"), "tests/snapshot/result_no_inconsistent_operating_states.mcf" ; "no_inconsistent_operating_states.mcf")]

#[test_case(include_str!("../../../examples/mCRL2/industrial/ieee-11073/no_successful_transmission_in_inconsistent_operating_states.mcf"), "tests/snapshot/result_no_successful_transmission_in_inconsistent_operating_states.mcf" ; "no_successful_transmission_in_inconsistent_operating_states.mcf")]

#[test_case(include_str!("../../../examples/mCRL2/modal-formulas/nolivelock.mcf"), "tests/snapshot/result_nolivelock.mcf" ; "nolivelock.mcf")]

#[test_case(include_str!("../../../examples/mCRL2/probabilistic/coin_tossing/formula1.mcf"), "tests/snapshot/result_formula1.mcf" ; "formula1.mcf")]

#[test_case(include_str!("../../../examples/mCRL2/probabilistic/coin_tossing/formula2.mcf"), "tests/snapshot/result_formula2.mcf" ; "formula2.mcf")]

// #[test_case(include_str!("../../../examples/mCRL2/probabilistic/slot_machines/1slot/expected_gain_1_run.mcf"), "tests/snapshot/result_expected_gain_1_run.mcf" ; "expected_gain_1_run.mcf")]

// #[test_case(include_str!("../../../examples/mCRL2/probabilistic/slot_machines/1slot/expected_gain_long_run.mcf"), "tests/snapshot/result_expected_gain_long_run.mcf" ; "expected_gain_long_run.mcf")]

// #[test_case(include_str!("../../../examples/mCRL2/probabilistic/slot_machines/1slot/expected_time_to_star.mcf"), "tests/snapshot/result_expected_time_to_star.mcf" ; "expected_time_to_star.mcf")]

// #[test_case(include_str!("../../../examples/mCRL2/probabilistic/slot_machines/3slot/expected_time_to_success.mcf"), "tests/snapshot/result_expected_time_to_success.mcf" ; "expected_time_to_success.mcf")]

// #[test_case(include_str!("../../../examples/mCRL2/probabilistic/slot_machines/3slot_hold/expected_probability_average.mcf"), "tests/snapshot/result_expected_probability_average.mcf" ; "expected_probability_average.mcf")]

// #[test_case(include_str!("../../../examples/mCRL2/probabilistic/slot_machines/3slot_hold/expected_probability_max.mcf"), "tests/snapshot/result_expected_probability_max.mcf" ; "expected_probability_max.mcf")]

// #[test_case(include_str!("../../../examples/mCRL2/probabilistic/slot_machines/3slot_hold/expected_probability_min.mcf"), "tests/snapshot/result_expected_probability_min.mcf" ; "expected_probability_min.mcf")]

// #[test_case(include_str!("../../../examples/mCRL2/probabilistic/slot_machines/paylines/expected_gain_10_run.mcf"), "tests/snapshot/result_expected_gain_10_run.mcf" ; "expected_gain_10_run.mcf")]

// #[test_case(include_str!("../../../examples/mCRL2/probabilistic/slot_machines/paylines/expected_gain_5_run.mcf"), "tests/snapshot/result_expected_gain_5_run.mcf" ; "expected_gain_5_run.mcf")]

// #[test_case(include_str!("../../../examples/mCRL2/probabilistic/slot_machines/reels_game/expected_gain_max_alt.mcf"), "tests/snapshot/result_expected_gain_max_alt.mcf" ; "expected_gain_max_alt.mcf")]

#[test_case(include_str!("../../../examples/mCRL2/probabilistic/spinning_mule_woolhouse/minimal_walking_distance.mcf"), "tests/snapshot/result_minimal_walking_distance.mcf" ; "minimal_walking_distance.mcf")]

#[test_case(include_str!("../../../examples/mCRL2/probabilistic/sultan_of_persia/best_spouse.mcf"), "tests/snapshot/result_best_spouse.mcf" ; "best_spouse.mcf")]

#[test_case(include_str!("../../../examples/mCRL2/software_models/Knuths_dancing_links/Dancing_links/properties/Correctness.mcf"), "tests/snapshot/result_correctness.mcf" ; "correctness.mcf")]

#[test_case(include_str!("../../../examples/mCRL2/software_models/Lamport_queue/properties/Head get set value.mcf"), "tests/snapshot/result_head_get_set_value.mcf" ; "head_get_set_value.mcf")]

#[test_case(include_str!("../../../examples/mCRL2/software_models/Lamport_queue/properties/Head not set out of bounds.mcf"), "tests/snapshot/result_head_not_set_out_of_bounds.mcf" ; "head_not_set_out_of_bounds.mcf")]

#[test_case(include_str!("../../../examples/mCRL2/software_models/Lamport_queue/properties/No out of bounds read.mcf"), "tests/snapshot/result_no_out_of_bounds_read.mcf" ; "no_out_of_bounds_read.mcf")]

#[test_case(include_str!("../../../examples/mCRL2/software_models/Lamport_queue/properties/No out of bounds write.mcf"), "tests/snapshot/result_no_out_of_bounds_write.mcf" ; "no_out_of_bounds_write.mcf")]

#[test_case(include_str!("../../../examples/mCRL2/software_models/Lamport_queue/properties/Pop always terminates.mcf"), "tests/snapshot/result_pop_always_terminates.mcf" ; "pop_always_terminates.mcf")]

#[test_case(include_str!("../../../examples/mCRL2/software_models/Lamport_queue/properties/Pop can terminate.mcf"), "tests/snapshot/result_pop_can_terminate.mcf" ; "pop_can_terminate.mcf")]

#[test_case(include_str!("../../../examples/mCRL2/software_models/Lamport_queue/properties/Push always terminates.mcf"), "tests/snapshot/result_push_always_terminates.mcf" ; "push_always_terminates.mcf")]

#[test_case(include_str!("../../../examples/mCRL2/software_models/Lamport_queue/properties/Push can terminate.mcf"), "tests/snapshot/result_push_can_terminate.mcf" ; "push_can_terminate.mcf")]

#[test_case(include_str!("../../../examples/mCRL2/software_models/Lamport_queue/properties/Queue behaviour.mcf"), "tests/snapshot/result_queue_behaviour.mcf" ; "queue_behaviour.mcf")]

#[test_case(include_str!("../../../examples/mCRL2/software_models/Lamport_queue/properties/Tail get set value.mcf"), "tests/snapshot/result_tail_get_set_value.mcf" ; "tail_get_set_value.mcf")]

#[test_case(include_str!("../../../examples/mCRL2/software_models/Lamport_queue/properties/Tail not read out of bounds.mcf"), "tests/snapshot/result_tail_not_read_out_of_bounds.mcf" ; "tail_not_read_out_of_bounds.mcf")]

#[test_case(include_str!("../../../examples/mCRL2/software_models/Lamport_queue/properties/Tail not set out of bounds.mcf"), "tests/snapshot/result_tail_not_set_out_of_bounds.mcf" ; "tail_not_set_out_of_bounds.mcf")]

#[test_case(include_str!("../../../examples/mCRL2/software_models/Treiber_stack/Treiber_CAS/properties/Correct release implies correct retrieve.mcf"), "tests/snapshot/result_correct_release_implies_correct_retrieve.mcf" ; "correct_release_implies_correct_retrieve.mcf")]

#[test_case(include_str!("../../../examples/mCRL2/software_models/Treiber_stack/Treiber_CAS/properties/Inevitably retrieve when stacksize is 2.mcf"), "tests/snapshot/result_inevitably_retrieve_when_stacksize_is_2.mcf" ; "inevitably_retrieve_when_stacksize_is_2.mcf")]

    }

#[cfg_attr(miri, ignore)]

#[test_case(include_str!("../../../examples/REC/mcrl2/add16.dataspec"), "tests/snapshot/result_add16.dataspec" ; "add16.dataspec")]

#[test_case(include_str!("../../../examples/REC/mcrl2/add32.dataspec"), "tests/snapshot/result_add32.dataspec" ; "add32.dataspec")]

#[test_case(include_str!("../../../examples/REC/mcrl2/add8.dataspec"), "tests/snapshot/result_add8.dataspec" ; "add8.dataspec")]

#[test_case(include_str!("../../../examples/REC/mcrl2/benchexpr10.dataspec"), "tests/snapshot/result_benchexpr10.dataspec" ; "benchexpr10.dataspec")]

#[test_case(include_str!("../../../examples/REC/mcrl2/benchexpr20.dataspec"), "tests/snapshot/result_benchexpr20.dataspec" ; "benchexpr20.dataspec")]

#[test_case(include_str!("../../../examples/REC/mcrl2/benchexpr22.dataspec"), "tests/snapshot/result_benchexpr22.dataspec" ; "benchexpr22.dataspec")]

#[test_case(include_str!("../../../examples/REC/mcrl2/benchsym10.dataspec"), "tests/snapshot/result_benchsym10.dataspec" ; "benchsym10.dataspec")]

#[test_case(include_str!("../../../examples/REC/mcrl2/benchsym20.dataspec"), "tests/snapshot/result_benchsym20.dataspec" ; "benchsym20.dataspec")]

#[test_case(include_str!("../../../examples/REC/mcrl2/benchsym22.dataspec"), "tests/snapshot/result_benchsym22.dataspec" ; "benchsym22.dataspec")]

#[test_case(include_str!("../../../examples/REC/mcrl2/benchtree10.dataspec"), "tests/snapshot/result_benchtree10.dataspec" ; "benchtree10.dataspec")]

#[test_case(include_str!("../../../examples/REC/mcrl2/benchtree20.dataspec"), "tests/snapshot/result_benchtree20.dataspec" ; "benchtree20.dataspec")]

#[test_case(include_str!("../../../examples/REC/mcrl2/benchtree22.dataspec"), "tests/snapshot/result_benchtree22.dataspec" ; "benchtree22.dataspec")]

#[test_case(include_str!("../../../examples/REC/mcrl2/binarysearch.dataspec"), "tests/snapshot/result_binarysearch.dataspec" ; "binarysearch.dataspec")]

#[test_case(include_str!("../../../examples/REC/mcrl2/bubblesort10.dataspec"), "tests/snapshot/result_bubblesort10.dataspec" ; "bubblesort10.dataspec")]

#[test_case(include_str!("../../../examples/REC/mcrl2/bubblesort100.dataspec"), "tests/snapshot/result_bubblesort100.dataspec" ; "bubblesort100.dataspec")]

#[test_case(include_str!("../../../examples/REC/mcrl2/bubblesort1000.dataspec"), "tests/snapshot/result_bubblesort1000.dataspec" ; "bubblesort1000.dataspec")]

#[test_case(include_str!("../../../examples/REC/mcrl2/bubblesort20.dataspec"), "tests/snapshot/result_bubblesort20.dataspec" ; "bubblesort20.dataspec")]

#[test_case(include_str!("../../../examples/REC/mcrl2/bubblesort720.dataspec"), "tests/snapshot/result_bubblesort720.dataspec" ; "bubblesort720.dataspec")]

#[test_case(include_str!("../../../examples/REC/mcrl2/calls.dataspec"), "tests/snapshot/result_calls.dataspec" ; "calls.dataspec")]

#[test_case(include_str!("../../../examples/REC/mcrl2/check1.dataspec"), "tests/snapshot/result_check1.dataspec" ; "check1.dataspec")]

#[test_case(include_str!("../../../examples/REC/mcrl2/check2.dataspec"), "tests/snapshot/result_check2.dataspec" ; "check2.dataspec")]

#[test_case(include_str!("../../../examples/REC/mcrl2/closure.dataspec"), "tests/snapshot/result_closure.dataspec" ; "closure.dataspec")]

#[test_case(include_str!("../../../examples/REC/mcrl2/confluence.dataspec"), "tests/snapshot/result_confluence.dataspec" ; "confluence.dataspec")]

#[test_case(include_str!("../../../examples/REC/mcrl2/dart.dataspec"), "tests/snapshot/result_dart.dataspec" ; "dart.dataspec")]

#[test_case(include_str!("../../../examples/REC/mcrl2/empty.dataspec"), "tests/snapshot/result_empty.dataspec" ; "empty.dataspec")]

#[test_case(include_str!("../../../examples/REC/mcrl2/evalexpr.dataspec"), "tests/snapshot/result_evalexpr.dataspec" ; "evalexpr.dataspec")]

#[test_case(include_str!("../../../examples/REC/mcrl2/evalsym.dataspec"), "tests/snapshot/result_evalsym.dataspec" ; "evalsym.dataspec")]

#[test_case(include_str!("../../../examples/REC/mcrl2/evaltree.dataspec"), "tests/snapshot/result_evaltree.dataspec" ; "evaltree.dataspec")]

#[test_case(include_str!("../../../examples/REC/mcrl2/factorial5.dataspec"), "tests/snapshot/result_factorial5.dataspec" ; "factorial5.dataspec")]

#[test_case(include_str!("../../../examples/REC/mcrl2/factorial6.dataspec"), "tests/snapshot/result_factorial6.dataspec" ; "factorial6.dataspec")]

#[test_case(include_str!("../../../examples/REC/mcrl2/factorial7.dataspec"), "tests/snapshot/result_factorial7.dataspec" ; "factorial7.dataspec")]

#[test_case(include_str!("../../../examples/REC/mcrl2/factorial8.dataspec"), "tests/snapshot/result_factorial8.dataspec" ; "factorial8.dataspec")]

#[test_case(include_str!("../../../examples/REC/mcrl2/factorial9.dataspec"), "tests/snapshot/result_factorial9.dataspec" ; "factorial9.dataspec")]

#[test_case(include_str!("../../../examples/REC/mcrl2/fib32.dataspec"), "tests/snapshot/result_fib32.dataspec" ; "fib32.dataspec")]

#[test_case(include_str!("../../../examples/REC/mcrl2/fibfree.dataspec"), "tests/snapshot/result_fibfree.dataspec" ; "fibfree.dataspec")]

#[test_case(include_str!("../../../examples/REC/mcrl2/fibonacci05.dataspec"), "tests/snapshot/result_fibonacci05.dataspec" ; "fibonacci05.dataspec")]

#[test_case(include_str!("../../../examples/REC/mcrl2/fibonacci18.dataspec"), "tests/snapshot/result_fibonacci18.dataspec" ; "fibonacci18.dataspec")]

#[test_case(include_str!("../../../examples/REC/mcrl2/fibonacci19.dataspec"), "tests/snapshot/result_fibonacci19.dataspec" ; "fibonacci19.dataspec")]

#[test_case(include_str!("../../../examples/REC/mcrl2/fibonacci20.dataspec"), "tests/snapshot/result_fibonacci20.dataspec" ; "fibonacci20.dataspec")]

#[test_case(include_str!("../../../examples/REC/mcrl2/fibonacci21.dataspec"), "tests/snapshot/result_fibonacci21.dataspec" ; "fibonacci21.dataspec")]

#[test_case(include_str!("../../../examples/REC/mcrl2/garbagecollection.dataspec"), "tests/snapshot/result_garbagecollection.dataspec" ; "garbagecollection.dataspec")]

#[test_case(include_str!("../../../examples/REC/mcrl2/hanoi12.dataspec"), "tests/snapshot/result_hanoi12.dataspec" ; "hanoi12.dataspec")]

#[test_case(include_str!("../../../examples/REC/mcrl2/hanoi16.dataspec"), "tests/snapshot/result_hanoi16.dataspec" ; "hanoi16.dataspec")]

#[test_case(include_str!("../../../examples/REC/mcrl2/hanoi20.dataspec"), "tests/snapshot/result_hanoi20.dataspec" ; "hanoi20.dataspec")]

#[test_case(include_str!("../../../examples/REC/mcrl2/hanoi4.dataspec"), "tests/snapshot/result_hanoi4.dataspec" ; "hanoi4.dataspec")]

#[test_case(include_str!("../../../examples/REC/mcrl2/hanoi8.dataspec"), "tests/snapshot/result_hanoi8.dataspec" ; "hanoi8.dataspec")]

#[test_case(include_str!("../../../examples/REC/mcrl2/intnat.dataspec"), "tests/snapshot/result_intnat.dataspec" ; "intnat.dataspec")]

#[test_case(include_str!("../../../examples/REC/mcrl2/langton6.dataspec"), "tests/snapshot/result_langton6.dataspec" ; "langton6.dataspec")]

#[test_case(include_str!("../../../examples/REC/mcrl2/langton7.dataspec"), "tests/snapshot/result_langton7.dataspec" ; "langton7.dataspec")]

#[test_case(include_str!("../../../examples/REC/mcrl2/logic3.dataspec"), "tests/snapshot/result_logic3.dataspec" ; "logic3.dataspec")]

#[test_case(include_str!("../../../examples/REC/mcrl2/maa.dataspec"), "tests/snapshot/result_maa.dataspec" ; "maa.dataspec")]

#[test_case(include_str!("../../../examples/REC/mcrl2/merge.dataspec"), "tests/snapshot/result_merge.dataspec" ; "merge.dataspec")]

#[test_case(include_str!("../../../examples/REC/mcrl2/mergesort10.dataspec"), "tests/snapshot/result_mergesort10.dataspec" ; "mergesort10.dataspec")]

#[test_case(include_str!("../../../examples/REC/mcrl2/mergesort100.dataspec"), "tests/snapshot/result_mergesort100.dataspec" ; "mergesort100.dataspec")]

#[test_case(include_str!("../../../examples/REC/mcrl2/mergesort1000.dataspec"), "tests/snapshot/result_mergesort1000.dataspec" ; "mergesort1000.dataspec")]

#[test_case(include_str!("../../../examples/REC/mcrl2/missionaries2.dataspec"), "tests/snapshot/result_missionaries2.dataspec" ; "missionaries2.dataspec")]

#[test_case(include_str!("../../../examples/REC/mcrl2/missionaries3.dataspec"), "tests/snapshot/result_missionaries3.dataspec" ; "missionaries3.dataspec")]

#[test_case(include_str!("../../../examples/REC/mcrl2/mul16.dataspec"), "tests/snapshot/result_mul16.dataspec" ; "mul16.dataspec")]

#[test_case(include_str!("../../../examples/REC/mcrl2/mul32.dataspec"), "tests/snapshot/result_mul32.dataspec" ; "mul32.dataspec")]

#[test_case(include_str!("../../../examples/REC/mcrl2/mul8.dataspec"), "tests/snapshot/result_mul8.dataspec" ; "mul8.dataspec")]

#[test_case(include_str!("../../../examples/REC/mcrl2/natlist.dataspec"), "tests/snapshot/result_natlist.dataspec" ; "natlist.dataspec")]

#[test_case(include_str!("../../../examples/REC/mcrl2/oddeven.dataspec"), "tests/snapshot/result_oddeven.dataspec" ; "oddeven.dataspec")]

#[test_case(include_str!("../../../examples/REC/mcrl2/omul32.dataspec"), "tests/snapshot/result_omul32.dataspec" ; "omul32.dataspec")]

#[test_case(include_str!("../../../examples/REC/mcrl2/omul8.dataspec"), "tests/snapshot/result_omul8.dataspec" ; "omul8.dataspec")]

#[test_case(include_str!("../../../examples/REC/mcrl2/order.dataspec"), "tests/snapshot/result_order.dataspec" ; "order.dataspec")]

#[test_case(include_str!("../../../examples/REC/mcrl2/permutations6.dataspec"), "tests/snapshot/result_permutations6.dataspec" ; "permutations6.dataspec")]

#[test_case(include_str!("../../../examples/REC/mcrl2/permutations7.dataspec"), "tests/snapshot/result_permutations7.dataspec" ; "permutations7.dataspec")]

#[test_case(include_str!("../../../examples/REC/mcrl2/quicksort10.dataspec"), "tests/snapshot/result_quicksort10.dataspec" ; "quicksort10.dataspec")]

#[test_case(include_str!("../../../examples/REC/mcrl2/quicksort100.dataspec"), "tests/snapshot/result_quicksort100.dataspec" ; "quicksort100.dataspec")]

#[test_case(include_str!("../../../examples/REC/mcrl2/quicksort1000.dataspec"), "tests/snapshot/result_quicksort1000.dataspec" ; "quicksort1000.dataspec")]

#[test_case(include_str!("../../../examples/REC/mcrl2/revelt.dataspec"), "tests/snapshot/result_revelt.dataspec" ; "revelt.dataspec")]

#[test_case(include_str!("../../../examples/REC/mcrl2/revnat100.dataspec"), "tests/snapshot/result_revnat100.dataspec" ; "revnat100.dataspec")]

#[test_case(include_str!("../../../examples/REC/mcrl2/revnat1000.dataspec"), "tests/snapshot/result_revnat1000.dataspec" ; "revnat1000.dataspec")]

#[test_case(include_str!("../../../examples/REC/mcrl2/revnat10000.dataspec"), "tests/snapshot/result_revnat10000.dataspec" ; "revnat10000.dataspec")]

#[test_case(include_str!("../../../examples/REC/mcrl2/searchinconditions.dataspec"), "tests/snapshot/result_searchinconditions.dataspec" ; "searchinconditions.dataspec")]

#[test_case(include_str!("../../../examples/REC/mcrl2/sieve100.dataspec"), "tests/snapshot/result_sieve100.dataspec" ; "sieve100.dataspec")]

#[test_case(include_str!("../../../examples/REC/mcrl2/sieve1000.dataspec"), "tests/snapshot/result_sieve1000.dataspec" ; "sieve1000.dataspec")]

#[test_case(include_str!("../../../examples/REC/mcrl2/sieve10000.dataspec"), "tests/snapshot/result_sieve10000.dataspec" ; "sieve10000.dataspec")]

#[test_case(include_str!("../../../examples/REC/mcrl2/sieve20.dataspec"), "tests/snapshot/result_sieve20.dataspec" ; "sieve20.dataspec")]

#[test_case(include_str!("../../../examples/REC/mcrl2/sieve2000.dataspec"), "tests/snapshot/result_sieve2000.dataspec" ; "sieve2000.dataspec")]

#[test_case(include_str!("../../../examples/REC/mcrl2/soundnessofparallelengines.dataspec"), "tests/snapshot/result_soundnessofparallelengines.dataspec" ; "soundnessofparallelengines.dataspec")]

#[test_case(include_str!("../../../examples/REC/mcrl2/tak18.dataspec"), "tests/snapshot/result_tak18.dataspec" ; "tak18.dataspec")]

#[test_case(include_str!("../../../examples/REC/mcrl2/tak36.dataspec"), "tests/snapshot/result_tak36.dataspec" ; "tak36.dataspec")]

#[test_case(include_str!("../../../examples/REC/mcrl2/tautologyhard.dataspec"), "tests/snapshot/result_tautologyhard.dataspec" ; "tautologyhard.dataspec")]

#[test_case(include_str!("../../../examples/REC/mcrl2/tricky.dataspec"), "tests/snapshot/result_tricky.dataspec" ; "tricky.dataspec")]

    }

#[cfg_attr(miri, ignore)]

// #[test_case(include_str!("../../../examples/mCRL2/pbes/datatypes.txt"), "tests/snapshot/result_datatypes.txt" ; "datatypes.txt")]

#[test_case(include_str!("../../../examples/mCRL2/pbes/nonmonotonic.txt"), "tests/snapshot/result_nonmonotonic.txt" ; "nonmonotonic.txt")]

#[test_case(include_str!("../../../examples/mCRL2/pbes/overloading.txt"), "tests/snapshot/result_overloading.txt" ; "overloading.txt")]

#[test_case(include_str!("../../../examples/mCRL2/pbes/true.txt"), "tests/snapshot/result_true.txt" ; "true.txt")]

    }