Grcov report - pbespgsolve

1

//! Compares our parity-game solver against mCRL2's `pbespgsolve` on random games written in the

2

//! textual PGSolver `.pg` format.

3

//!

4

//! Gated on `MCRL2_PATH`: skipped in the default test run (when the variable is unset) and

5

//! exercised by the dedicated mCRL2 CI job. Set `MERC_DUMP` to keep the generated `.pg` files for a

6

//! failing seed.

7

8

use std::path::Path;

9

use std::process::Command;

10

11

use merc_io::temp_dir;

12

use merc_utilities::random_test;

13

use merc_vpg::Player;

14

use merc_vpg::random_parity_game;

15

use merc_vpg::solve_zielonka;

16

use merc_vpg::write_pg;

17

18

/// Compares the winner of the initial vertex (index 0) computed by our Zielonka solver against

19

/// `pbespgsolve` on random total parity games.

20

#[test]

21

#[cfg_attr(miri, ignore)]

22

1

fn test_mcrl2_pbespgsolve_vs_zielonka() {

23

1

    let Ok(mcrl2_path) = std::env::var("MCRL2_PATH") else {

24

1

        println!("Skipping test: MCRL2_PATH not set");

25

1

        return;

26

};

27

28

    let pbespgsolve = Path::new(&mcrl2_path).join("pbespgsolve");

29

30

    random_test(100, |rng| {

31

        // A total game with a modest size and priority range keeps pbespgsolve fast while still

32

        // producing a variety of winner partitions. Zielonka requires the game to be total.

33

        let game = random_parity_game(rng, true, 50, 5, 3);

34

35

        let dir = temp_dir("pbespgsolve").unwrap();

36

        let input_path = dir.path().join("input.pg");

37

38

            let mut file = std::fs::File::create(&input_path).unwrap();

39

            write_pg(&mut file, &game).unwrap();

40

41

42

        // pbespgsolve solves the game and reports whether the initial vertex (index 0) is won by

43

        // player Even (player 0): "true" means Even wins, "false" means Odd wins. This matches the

44

        // PGSolver/mCRL2 convention where owner 0 is the player favouring even priorities.

45

        let output = Command::new(&pbespgsolve)

46

            .arg(&input_path)

47

            .output()

48

            .expect("Failed to run pbespgsolve");

49

        assert!(

50

            output.status.success(),

51

            "pbespgsolve failed: {}",

52

            String::from_utf8_lossy(&output.stderr)

53

);

54

55

        let stdout = String::from_utf8_lossy(&output.stdout);

56

        let mcrl2_even_wins = if stdout.contains("true") {

57

            true

58

        } else if stdout.contains("false") {

59

            false

60

        } else {

61

            panic!("Unexpected pbespgsolve output: {stdout:?}");

62

};

63

64

        // Our solver: the initial vertex is won by Even iff it lies in the Even winning set.

65

        let (solution, _) = solve_zielonka(&game, false);

66

        let our_even_wins: bool = solution[Player::Even.to_index()][0];

67

68

        assert_eq!(

69

            our_even_wins, mcrl2_even_wins,

70

            "Winner of the initial vertex differs from pbespgsolve",

71

);

72

});

73

1