Grcov report - symbolic

1

use std::ops::Range;

2

3

use oxidd::BooleanFunctionQuant;

4

use oxidd::BooleanOperator;

5

use oxidd::FunctionSubst;

6

use oxidd::Manager;

7

use oxidd::ManagerRef;

8

use oxidd::Subst;

9

use oxidd::VarNo;

10

use oxidd::bdd::BDDFunction;

11

use oxidd::bdd::BDDManagerRef;

12

use oxidd::error::DuplicateVarName;

13

use oxidd::ldd::Value;

14

15

use merc_utilities::MercError;

16

17

use crate::SummandGroupBdd;

18

use crate::SymbolicLtsBdd;

19

use crate::compute_vars_bdd;

20

use crate::variable_rename_reverse;

21

22

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

23

///

24

/// # Details

25

///

26

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

27

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

28

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

29

///

30

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

31

100

pub fn quotient_symbolic(

32

100

    manager_ref: &BDDManagerRef,

33

100

    lts: &SymbolicLtsBdd,

34

100

    partition: &BDDFunction,

35

100

    block_vars: &[VarNo],

36

100

) -> Result<SymbolicLtsBdd, MercError> {

37

100

    let num_block_bits = block_vars.len();

38

39

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

40

100

    let next_block_names = (0..num_block_bits)

41

393

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

42

100

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

43

100

    let next_block_vars: Vec<VarNo> = manager_ref

44

100

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

45

100

            manager.add_named_vars(next_block_names)

46

100

})

47

100

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

48

100

        .collect();

49

50

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

51

100

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

52

100

        .state_variables()

53

100

        .iter()

54

100

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

55

2997

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

56

100

        .collect();

57

100

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

58

59

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

60

100

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

61

100

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

62

63

    // Cubes to quantify over.

64

100

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

65

100

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

66

67

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

68

100

    let states_q = lts

69

100

        .states()

70

100

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

71

72

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

73

100

    let initial_state_q = lts

74

100

        .initial_state()

75

100

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

76

77

    // 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').

78

//

79

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

80

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

81

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

82

100

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

83

500

    for group in lts.transition_groups() {

84

500

        let extended = crate::extend_relation(

85

500

            manager_ref,

86

500

            group.relation(),

87

500

            lts.state_variables(),

88

500

            lts.next_state_variables(),

89

500

            group.write_variables(),

90

)?;

91

92

500

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

93

500

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

94

95

500

        quotient_groups.push(SummandGroupBdd::new(

96

500

            quotient,

97

500

            block_vars.to_vec(),

98

500

            next_block_vars.clone(),

99

));

100

101

102

100

    Ok(SymbolicLtsBdd::with_quotient_state(

103

100

        lts,

104

100

        states_q,

105

100

        initial_state_q,

106

100

        quotient_groups,

107

100

        block_vars.to_vec(),

108

100

        next_block_vars,

109

100

        vec![num_block_bits as Value],

110

100

))

111

100