Grcov report - symbolic

1

use std::ops::Range;

2

3

use merc_ldd::Value;

4

use merc_utilities::MercError;

5

use oxidd::BooleanFunctionQuant;

6

use oxidd::BooleanOperator;

7

use oxidd::FunctionSubst;

8

use oxidd::Manager;

9

use oxidd::ManagerRef;

10

use oxidd::Subst;

11

use oxidd::VarNo;

12

use oxidd::bdd::BDDFunction;

13

use oxidd::bdd::BDDManagerRef;

14

use oxidd::error::DuplicateVarName;

15

16

use crate::SummandGroupBdd;

17

use crate::SymbolicLtsBdd;

18

use crate::compute_vars_bdd;

19

use crate::variable_rename_reverse;

20

21

/// Computes the symbolic quotient of the given partition.

22

///

23

/// # Details

24

///

25

/// The returned LTS encodes its states as block indices over the supplied

26

/// `block_vars` (used as the source-block bits) and over a freshly allocated

27

/// set of "next-block" variables (used as the target-block bits).

28

///

29

/// The action variables and action labels are inherited from `lts`.

30

100

pub fn quotient_symbolic(

31

100

    manager_ref: &BDDManagerRef,

32

100

    lts: &SymbolicLtsBdd,

33

100

    partition: &BDDFunction,

34

100

    block_vars: &[VarNo],

35

100

) -> Result<SymbolicLtsBdd, MercError> {

36

100

    let num_block_bits = block_vars.len();

37

38

    // Allocate next-block variables in the manager (one per source-block bit).

39

100

    let next_block_names = (0..num_block_bits)

40

373

        .map(|i| format!("nb_{}", i))

41

100

        .collect::<Vec<String>>();

42

100

    let next_block_vars: Vec<VarNo> = manager_ref

43

100

        .with_manager_exclusive(|manager| -> Result<Range<VarNo>, DuplicateVarName> {

44

100

            manager.add_named_vars(next_block_names)

45

100

})

46

100

        .map_err(|e| format!("Failed to create next-block variables: {e}"))?

47

100

        .collect();

48

49

    // P_source(s, b) = P(s', b)[s' <- s]

50

100

    let s_prime_to_s_pairs: Vec<(VarNo, VarNo)> = lts

51

100

        .state_variables()

52

100

        .iter()

53

100

        .zip(lts.next_state_variables().iter())

54

2999

        .map(|(s, s_prime)| (*s_prime, *s))

55

100

        .collect();

56

100

    let partition_source = variable_rename_reverse(manager_ref, partition, &s_prime_to_s_pairs)?;

57

58

    // P_target(s', b') = P(s', b)[b <- b']

59

100

    let (next_block_vars_bdd, _) = compute_vars_bdd(manager_ref, &next_block_vars)?;

60

100

    let partition_target = partition.substitute(&Subst::new(block_vars, &next_block_vars_bdd))?;

61

62

    // Cubes to quantify over.

63

100

    let (_, state_vars_bdd) = compute_vars_bdd(manager_ref, lts.state_variables())?;

64

100

    let (_, next_state_vars_bdd) = compute_vars_bdd(manager_ref, lts.next_state_variables())?;

65

66

    // States_q(b) = ∃ s. states(s) ∧ P_source(s, b)

67

100

    let states_q = lts

68

100

        .states()

69

100

        .apply_exists(BooleanOperator::And, &partition_source, &state_vars_bdd)?;

70

71

    // InitialState_q(b) = ∃ s. initial_state(s) ∧ P_source(s, b)

72

100

    let initial_state_q = lts

73

100

        .initial_state()

74

100

        .apply_exists(BooleanOperator::And, &partition_source, &state_vars_bdd)?;

75

76

    // For each transition group, compute T_q(b, b', a) = ∃ s, s'. T_ext(s, s', a) ∧ P_source(s, b) ∧ P_target(s', b').

77

//

78

    // The relation is extended with x = x' for non-written state variables so the existential

79

    // quantification does not leave those variables unconstrained — otherwise non-written next-state

80

    // bits would be free and we would conflate transitions with different target states.

81

100

    let mut quotient_groups = Vec::with_capacity(lts.transition_groups().len());

82

500

    for group in lts.transition_groups() {

83

500

        let extended = crate::sigref::extend_relation(

84

500

            manager_ref,

85

500

            group.relation(),

86

500

            lts.state_variables(),

87

500

            lts.next_state_variables(),

88

500

            group.write_variables(),

89

)?;

90

91

500

        let tmp = extended.apply_exists(BooleanOperator::And, &partition_target, &next_state_vars_bdd)?;

92

500

        let quotient = tmp.apply_exists(BooleanOperator::And, &partition_source, &state_vars_bdd)?;

93

94

500

        quotient_groups.push(SummandGroupBdd::new(

95

500

            quotient,

96

500

            block_vars.to_vec(),

97

500

            next_block_vars.clone(),

98

));

99

100

101

100

    Ok(SymbolicLtsBdd::with_quotient_state(

102

100

        lts,

103

100

        states_q,

104

100

        initial_state_q,

105

100

        quotient_groups,

106

100

        block_vars.to_vec(),

107

100

        next_block_vars,

108

100

        vec![num_block_bits as Value],

109

100

))

110

100