1 
//! Authors: Maurice Laveaux, Eduardo Costa Martins
2 
//!
3 
//! Implements the weak bisimulation algorithm by Eduardo Costa Martins.
4 
#![forbid(unsafe_code)]
5 

            

        

            

                6
            

            

                
            

            

                
use std::iter;

            

        

            

                7
            

            

                
            

            

                

            

        

            

                8
            

            

                
            

            

                
use bitvec::bitvec;

            

        

            

                9
            

            

                
            

            

                
use bitvec::order::Lsb0;

            

        

            

                10
            

            

                
            

            

                

            

        

            

                11
            

            

                
            

            

                
use bitvec::vec::BitVec;

            

        

            

                12
            

            

                
            

            

                
use log::info;

            

        

            

                13
            

            

                
            

            

                
use log::trace;

            

        

            

                14
            

            

                
            

            

                
use merc_collections::BlockIndex;

            

        

            

                15
            

            

                
            

            

                
use merc_io::TimeProgress;

            

        

            

                16
            

            

                
            

            

                
use merc_lts::IncomingTransitions;

            

        

            

                17
            

            

                
            

            

                
use merc_lts::LTS;

            

        

            

                18
            

            

                
            

            

                
use merc_lts::LabelIndex;

            

        

            

                19
            

            

                
            

            

                
use merc_lts::LabelledTransitionSystem;

            

        

            

                20
            

            

                
            

            

                
use merc_lts::StateIndex;

            

        

            

                21
            

            

                
            

            

                
use merc_utilities::Timing;

            

        

            

                22
            

            

                
            

            

                

            

        

            

                23
            

            

                
            

            

                
use crate::Equivalence;

            

        

            

                24
            

            

                
            

            

                
use crate::MarkedBlockPartition;

            

        

            

                25
            

            

                
            

            

                
use crate::reduce_lts;

            

        

            

                26
            

            

                
            

            

                
use crate::tau_loop_elimination_and_reorder;

            

        

            

                27
            

            

                
            

            

                

            

        

            

                28
            

            

                
            

            

                
/// Type alias because we use bitvec for marking states

            

        

            

                29
            

            

                
            

            

                
type BitArray = BitVec<u64, Lsb0>;

            

        

            

                30
            

            

                
            

            

                

            

        

            

                31
            

            

                
            

            

                
/// Apply weak bisimulation reduction

            

        

            

                32
            

            

                
            

            

                
///

            

        

            

                33
            

            

                
            

            

                
/// # Details

            

        

            

                34
            

            

                
            

            

                
///

            

        

            

                35
            

            

                
            

            

                
/// The `preprocess` flag indicates whether to preprocess the LTS using

            

        

            

                36
            

            

                
            

            

                
/// branching bisimulation.

            

        

            

                37
            

            

                
            

            

                
/// 

            

        

            

                38
            

            

                
            

            

                
/// The `state` is any state for which we return the equivalent state in the

            

        

            

                39
            

            

                
            

            

                
/// preprocessed LTS.

            

        

            

                40
            

            

                400
            

            

                
pub fn weak_bisimulation<L: LTS>(

            

        

            

                41
            

            

                400
            

            

                
    lts: L,

            

        

            

                42
            

            

                400
            

            

                
    state: StateIndex,

            

        

            

                43
            

            

                400
            

            

                
    preprocess: bool,

            

        

            

                44
            

            

                400
            

            

                
    timing: &Timing,

            

        

            

                45
            

            

                400
            

            

                
) -> (LabelledTransitionSystem<L::Label>, StateIndex, MarkedBlockPartition) {

            

        

            

                46
            

            

                
            

            

                
    // Preprocess the LTS if desired.

            

        

            

                47
            

            

                400
            

            

                
    if preprocess {

            

        

            

                48
            

            

                
            

            

                
        let lts = timing.measure("preprocess", || {

            

        

            

                49
            

            

                
            

            

                
            reduce_lts(lts, Equivalence::BranchingBisim, true, timing)

            

        

            

                50
            

            

                
            

            

                
        });

            

        

            

                51
            

            

                
            

            

                
        weak_bisimulation_impl(lts, state, timing)

            

        

            

                52
            

            

                
            

            

                
    } else {

            

        

            

                53
            

            

                400
            

            

                
        weak_bisimulation_impl(lts, state, timing)

            

        

            

                54
            

            

                
            

            

                
    }

            

        

            

                55
            

            

                400
            

            

                
}

            

        

            

                56
            

            

                
            

            

                

            

        

            

                57
            

            

                
            

            

                
/// Apply weak bisimulation reduction using the parallel variant of the

            

        

            

                58
            

            

                
            

            

                
/// algorithm

            

        

            

                59
            

            

                
            

            

                
///

            

        

            

                60
            

            

                
            

            

                
/// # Details

            

        

            

                61
            

            

                
            

            

                
///

            

        

            

                62
            

            

                
            

            

                
/// The `preprocess` flag indicates whether to preprocess the LTS using

            

        

            

                63
            

            

                
            

            

                
/// branching bisimulation.

            

        

            

                64
            

            

                
            

            

                
/// 

            

        

            

                65
            

            

                
            

            

                
/// The `state` is any state for which we return the equivalent state in the

            

        

            

                66
            

            

                
            

            

                
/// preprocessed LTS.

            

        

            

                67
            

            

                300
            

            

                
pub fn weak_bisimulation_parallel<L: LTS>(

            

        

            

                68
            

            

                300
            

            

                
    lts: L,

            

        

            

                69
            

            

                300
            

            

                
    state: StateIndex,

            

        

            

                70
            

            

                300
            

            

                
    preprocess: bool,

            

        

            

                71
            

            

                300
            

            

                
    timing: &Timing,

            

        

            

                72
            

            

                300
            

            

                
) -> (LabelledTransitionSystem<L::Label>, StateIndex, MarkedBlockPartition) {

            

        

            

                73
            

            

                
            

            

                
    // Preprocess the LTS if desired.

            

        

            

                74
            

            

                300
            

            

                
    if preprocess {

            

        

            

                75
            

            

                
            

            

                
        let lts = timing.measure("preprocess", || {

            

        

            

                76
            

            

                
            

            

                
            reduce_lts(lts, Equivalence::BranchingBisim, true, timing)

            

        

            

                77
            

            

                
            

            

                
        });

            

        

            

                78
            

            

                
            

            

                
        weak_bisimulation_parallel_impl(lts, state, timing)

            

        

            

                79
            

            

                
            

            

                
    } else {

            

        

            

                80
            

            

                300
            

            

                
        weak_bisimulation_parallel_impl(lts, state, timing)

            

        

            

                81
            

            

                
            

            

                
    }

            

        

            

                82
            

            

                300
            

            

                
}

            

        

            

                83
            

            

                
            

            

                

            

        

            

                84
            

            

                
            

            

                
/// Core weak bisimulation algorithm implementation.

            

        

            

                85
            

            

                400
            

            

                
fn weak_bisimulation_impl<L: LTS>(

            

        

            

                86
            

            

                400
            

            

                
    lts: L,

            

        

            

                87
            

            

                400
            

            

                
    state: StateIndex,

            

        

            

                88
            

            

                400
            

            

                
    timing: &Timing,

            

        

            

                89
            

            

                400
            

            

                
) -> (LabelledTransitionSystem<L::Label>, StateIndex, MarkedBlockPartition) {

            

        

            

                90
            

            

                400
            

            

                
    let (tau_loop_free_lts, mapped_state) = timing.measure("preprocess", || tau_loop_elimination_and_reorder(lts, state));

            

        

            

                91
            

            

                
            

            

                

            

        

            

                92
            

            

                400
            

            

                
    timing.measure("reduction", || {

            

        

            

                93
            

            

                400
            

            

                
        let mut blocks = MarkedBlockPartition::new(tau_loop_free_lts.num_of_states());

            

        

            

                94
            

            

                
            

            

                

            

        

            

                95
            

            

                400
            

            

                
        let mut act_mark = bitvec![u64, Lsb0; 0; tau_loop_free_lts.num_of_states()];

            

        

            

                96
            

            

                400
            

            

                
        let mut tau_mark = bitvec![u64, Lsb0; 0; tau_loop_free_lts.num_of_states()];

            

        

            

                97
            

            

                
            

            

                

            

        

            

                98
            

            

                400
            

            

                
        let incoming = IncomingTransitions::new(&tau_loop_free_lts);

            

        

            

                99
            

            

                
            

            

                

            

        

            

                100
            

            

                400
            

            

                
        let progress = TimeProgress::new(

            

        

            

                101
            

            

                20
            

            

                
            |num_of_blocks: usize| {

            

        

            

                102
            

            

                20
            

            

                
                info!("Found {} blocks...", num_of_blocks);

            

        

            

                103
            

            

                20
            

            

                
            },

            

        

            

                104
            

            

                
            

            

                
            1,

            

        

            

                105
            

            

                
            

            

                
        );

            

        

            

                106
            

            

                
            

            

                

            

        

            

                107
            

            

                
            

            

                
        loop {

            

        

            

                108
            

            

                1266
            

            

                
            let mut stable = true;

            

        

            

                109
            

            

                12818
            

            

                
            for block_index in (0usize..blocks.num_of_blocks()).map(BlockIndex::new) {

            

        

            

                110
            

            

                12818
            

            

                
                progress.print(blocks.num_of_blocks());

            

        

            

                111
            

            

                12818
            

            

                
                if *blocks.block(block_index).annotation() {

            

        

            

                112
            

            

                8127
            

            

                
                    continue;

            

        

            

                113
            

            

                4691
            

            

                
                }

            

        

            

                114
            

            

                
            

            

                

            

        

            

                115
            

            

                4691
            

            

                
                trace!("Stabilising block {:?}", block_index);

            

        

            

                116
            

            

                4691
            

            

                
                stable = false;

            

        

            

                117
            

            

                4691
            

            

                
                blocks.mark_block_stable(block_index);

            

        

            

                118
            

            

                
            

            

                

            

        

            

                119
            

            

                
            

            

                
                // tau is the first label.

            

        

            

                120
            

            

                42219
            

            

                
                for label in tau_loop_free_lts

            

        

            

                121
            

            

                4691
            

            

                
                    .labels()

            

        

            

                122
            

            

                4691
            

            

                
                    .iter()

            

        

            

                123
            

            

                4691
            

            

                
                    .enumerate()

            

        

            

                124
            

            

                42219
            

            

                
                    .map(|(i, _)| LabelIndex::new(i))

            

        

            

                125
            

            

                
            

            

                
                {

            

        

            

                126
            

            

                42219
            

            

                
                    compute_weak_act(

            

        

            

                127
            

            

                42219
            

            

                
                        &mut act_mark,

            

        

            

                128
            

            

                42219
            

            

                
                        &mut tau_mark,

            

        

            

                129
            

            

                42219
            

            

                
                        &tau_loop_free_lts,

            

        

            

                130
            

            

                42219
            

            

                
                        &blocks,

            

        

            

                131
            

            

                42219
            

            

                
                        &incoming,

            

        

            

                132
            

            

                42219
            

            

                
                        block_index,

            

        

            

                133
            

            

                42219
            

            

                
                        label,

            

        

            

                134
            

            

                
            

            

                
                    );

            

        

            

                135
            

            

                
            

            

                

            

        

            

                136
            

            

                
            

            

                
                    // Note that we cannot use the block references here, and instead uses indices, because stabilise

            

        

            

                137
            

            

                
            

            

                
                    // also modifies the blocks structure.

            

        

            

                138
            

            

                3464876
            

            

                
                    for block_prime in (0usize..blocks.num_of_blocks()).map(BlockIndex::new) {

            

        

            

                139
            

            

                3464876
            

            

                
                        stabilise(block_prime, &mut act_mark, &mut blocks);

            

        

            

                140
            

            

                3464876
            

            

                
                    }

            

        

            

                141
            

            

                
            

            

                
                }

            

        

            

                142
            

            

                
            

            

                
            }

            

        

            

                143
            

            

                
            

            

                

            

        

            

                144
            

            

                1266
            

            

                
            if stable {

            

        

            

                145
            

            

                
            

            

                
                // Quit the outer loop.

            

        

            

                146
            

            

                400
            

            

                
                trace!("Partition is stable!");

            

        

            

                147
            

            

                400
            

            

                
                break;

            

        

            

                148
            

            

                866
            

            

                
            }

            

        

            

                149
            

            

                
            

            

                
        }

            

        

            

                150
            

            

                
            

            

                

            

        

            

                151
            

            

                400
            

            

                
        (tau_loop_free_lts, mapped_state, blocks)

            

        

            

                152
            

            

                400
            

            

                
    })

            

        

            

                153
            

            

                400
            

            

                
}

            

        

            

                154
            

            

                
            

            

                

            

        

            

                155
            

            

                300
            

            

                
fn weak_bisimulation_parallel_impl<L: LTS>(

            

        

            

                156
            

            

                300
            

            

                
    lts: L,

            

        

            

                157
            

            

                300
            

            

                
    state: StateIndex,

            

        

            

                158
            

            

                300
            

            

                
    timing: &Timing,

            

        

            

                159
            

            

                300
            

            

                
) -> (LabelledTransitionSystem<L::Label>, StateIndex, MarkedBlockPartition) {

            

        

            

                160
            

            

                300
            

            

                
    let (tau_loop_free_lts, mapped_state) = timing.measure("preprocess", || tau_loop_elimination_and_reorder(lts, state));

            

        

            

                161
            

            

                
            

            

                

            

        

            

                162
            

            

                300
            

            

                
    let progress = TimeProgress::new(

            

        

            

                163
            

            

                
            

            

                
        |num_of_blocks: usize| {

            

        

            

                164
            

            

                
            

            

                
            info!("Found {} blocks...", num_of_blocks);

            

        

            

                165
            

            

                
            

            

                
        },

            

        

            

                166
            

            

                
            

            

                
        1,

            

        

            

                167
            

            

                
            

            

                
    );

            

        

            

                168
            

            

                
            

            

                

            

        

            

                169
            

            

                300
            

            

                
    timing.measure("reduction", || {

            

        

            

                170
            

            

                300
            

            

                
        let mut blocks = MarkedBlockPartition::new(tau_loop_free_lts.num_of_states());

            

        

            

                171
            

            

                
            

            

                

            

        

            

                172
            

            

                
            

            

                
        // Represents the s.marked[a] from the pseudocode.

            

        

            

                173
            

            

                300
            

            

                
        let mut marked = Vec::from_iter(iter::repeat_n(

            

        

            

                174
            

            

                300
            

            

                
            bitvec![u64, Lsb0; 0; tau_loop_free_lts.labels().len()],

            

        

            

                175
            

            

                300
            

            

                
            tau_loop_free_lts.num_of_states(),

            

        

            

                176
            

            

                
            

            

                
        ));

            

        

            

                177
            

            

                
            

            

                

            

        

            

                178
            

            

                300
            

            

                
        let incoming = IncomingTransitions::new(&tau_loop_free_lts);

            

        

            

                179
            

            

                
            

            

                

            

        

            

                180
            

            

                
            

            

                
        loop {

            

        

            

                181
            

            

                893
            

            

                
            let mut stable = true;

            

        

            

                182
            

            

                3970
            

            

                
            for block_index in (0usize..blocks.num_of_blocks()).map(BlockIndex::new) {

            

        

            

                183
            

            

                3970
            

            

                
                progress.print(blocks.num_of_blocks());

            

        

            

                184
            

            

                3970
            

            

                
                if *blocks.block(block_index).annotation() {

            

        

            

                185
            

            

                2220
            

            

                
                    continue;

            

        

            

                186
            

            

                1750
            

            

                
                }

            

        

            

                187
            

            

                
            

            

                

            

        

            

                188
            

            

                1750
            

            

                
                trace!("Stabilising block {:?}", block_index);

            

        

            

                189
            

            

                1750
            

            

                
                stable = false;

            

        

            

                190
            

            

                1750
            

            

                
                blocks.mark_block_stable(block_index);

            

        

            

                191
            

            

                
            

            

                

            

        

            

                192
            

            

                
            

            

                
                // marked := 0 for all states and actions

            

        

            

                193
            

            

                54729
            

            

                
                for act_mark in &mut marked {

            

        

            

                194
            

            

                54729
            

            

                
                    act_mark.fill(false);

            

        

            

                195
            

            

                54729
            

            

                
                }

            

        

            

                196
            

            

                
            

            

                

            

        

            

                197
            

            

                1750
            

            

                
                compute_weak_acts(&mut marked, &tau_loop_free_lts, &incoming, &blocks, block_index);

            

        

            

                198
            

            

                
            

            

                

            

        

            

                199
            

            

                2548
            

            

                
                while let Some(label) = find_act(&tau_loop_free_lts, &blocks, &mut marked) {

            

        

            

                200
            

            

                9774
            

            

                
                    for block_index in (0usize..blocks.num_of_blocks()).map(BlockIndex::new) {

            

        

            

                201
            

            

                9774
            

            

                
                        stabilise_act(block_index, label, &mut marked, &mut blocks);

            

        

            

                202
            

            

                9774
            

            

                
                    }

            

        

            

                203
            

            

                
            

            

                
                }

            

        

            

                204
            

            

                
            

            

                
            }

            

        

            

                205
            

            

                
            

            

                

            

        

            

                206
            

            

                893
            

            

                
            if stable {

            

        

            

                207
            

            

                
            

            

                
                // Quit the outer loop.

            

        

            

                208
            

            

                300
            

            

                
                trace!("Partition is stable!");

            

        

            

                209
            

            

                300
            

            

                
                break;

            

        

            

                210
            

            

                593
            

            

                
            }

            

        

            

                211
            

            

                
            

            

                
        }

            

        

            

                212
            

            

                
            

            

                

            

        

            

                213
            

            

                300
            

            

                
        (tau_loop_free_lts, mapped_state, blocks)

            

        

            

                214
            

            

                300
            

            

                
    })

            

        

            

                215
            

            

                300
            

            

                
}

            

        

            

                216
            

            

                
            

            

                

            

        

            

                217
            

            

                
            

            

                
/// Sets s.act_mark to true iff exists t: S. s =\not{a}=> t

            

        

            

                218
            

            

                
            

            

                
/// If a = tau, then also updates s.tau_mark

            

        

            

                219
            

            

                57969
            

            

                
fn compute_weak_act<L: LTS>(

            

        

            

                220
            

            

                57969
            

            

                
    act_mark: &mut BitArray,

            

        

            

                221
            

            

                57969
            

            

                
    tau_mark: &mut BitArray,

            

        

            

                222
            

            

                57969
            

            

                
    lts: &L,

            

        

            

                223
            

            

                57969
            

            

                
    blocks: &MarkedBlockPartition,

            

        

            

                224
            

            

                57969
            

            

                
    incoming: &IncomingTransitions,

            

        

            

                225
            

            

                57969
            

            

                
    block: BlockIndex,

            

        

            

                226
            

            

                57969
            

            

                
    label: LabelIndex,

            

        

            

                227
            

            

                57969
            

            

                
) {

            

        

            

                228
            

            

                12757806
            

            

                
    for s in lts.iter_states() {

            

        

            

                229
            

            

                
            

            

                
        // s.act_mark := true iff s in B && a == tau

            

        

            

                230
            

            

                12757806
            

            

                
        act_mark.set(

            

        

            

                231
            

            

                12757806
            

            

                
            *s,

            

        

            

                232
            

            

                12757806
            

            

                
            lts.is_hidden_label(label) && blocks.iter_block(block).any(|state| state == *s),

            

        

            

                233
            

            

                
            

            

                
        );

            

        

            

                234
            

            

                
            

            

                

            

        

            

                235
            

            

                34278417
            

            

                
        for transition in lts.outgoing_transitions(s) {

            

        

            

                236
            

            

                34278417
            

            

                
            if transition.label == label {

            

        

            

                237
            

            

                
            

            

                
                // s.act_mark := true iff a != tau && tau_mark[t]

            

        

            

                238
            

            

                3808713
            

            

                
                if !lts.is_hidden_label(transition.label) && tau_mark[*transition.to] {

            

        

            

                239
            

            

                50528
            

            

                
                    act_mark.set(*s, true);

            

        

            

                240
            

            

                3758185
            

            

                
                }

            

        

            

                241
            

            

                30469704
            

            

                
            }

            

        

            

                242
            

            

                
            

            

                
        }

            

        

            

                243
            

            

                
            

            

                
    }

            

        

            

                244
            

            

                
            

            

                

            

        

            

                245
            

            

                12757806
            

            

                
    for t in lts.iter_states() {

            

        

            

                246
            

            

                
            

            

                
        // t.tau_mark := t.act_mark if a == tau

            

        

            

                247
            

            

                12757806
            

            

                
        if lts.is_hidden_label(label) {

            

        

            

                248
            

            

                1417534
            

            

                
            tau_mark.set(*t, act_mark[*t]);

            

        

            

                249
            

            

                11340272
            

            

                
        }

            

        

            

                250
            

            

                
            

            

                

            

        

            

                251
            

            

                12757806
            

            

                
        if act_mark[*t] {

            

        

            

                252
            

            

                88287
            

            

                
            for transition in incoming.incoming_silent_transitions(t) {

            

        

            

                253
            

            

                49105
            

            

                
                act_mark.set(*transition.from, true);

            

        

            

                254
            

            

                49105
            

            

                
            }

            

        

            

                255
            

            

                12669519
            

            

                
        }

            

        

            

                256
            

            

                
            

            

                
    }

            

        

            

                257
            

            

                57969
            

            

                
}

            

        

            

                258
            

            

                
            

            

                

            

        

            

                259
            

            

                
            

            

                
/// Computing weak reachability for all actions at once. The `marked` array contains |Act| entries per state.

            

        

            

                260
            

            

                
            

            

                
///

            

        

            

                261
            

            

                
            

            

                
/// # Details

            

        

            

                262
            

            

                
            

            

                
///

            

        

            

                263
            

            

                
            

            

                
/// Requires s.tau_mark iff s ->> B.

            

        

            

                264
            

            

                
            

            

                
/// For all a in A sets s.marked[a] iff s =[a]> B.

            

        

            

                265
            

            

                
            

            

                
///

            

        

            

                266
            

            

                
            

            

                
/// Note that `B` is only used for debugging checks, and is not used in the actual algorithm.

            

        

            

                267
            

            

                1750
            

            

                
fn compute_weak_acts<L: LTS>(

            

        

            

                268
            

            

                1750
            

            

                
    marked: &mut [BitArray],

            

        

            

                269
            

            

                1750
            

            

                
    lts: &L,

            

        

            

                270
            

            

                1750
            

            

                
    incoming: &IncomingTransitions<'_>,

            

        

            

                271
            

            

                1750
            

            

                
    blocks: &MarkedBlockPartition,

            

        

            

                272
            

            

                1750
            

            

                
    block: BlockIndex,

            

        

            

                273
            

            

                1750
            

            

                
) {

            

        

            

                274
            

            

                1750
            

            

                
    if cfg!(debug_assertions) {

            

        

            

                275
            

            

                
            

            

                
        // Check that compute_weak_act results in the same markings as the optimised compute_weak_acts procedure.

            

        

            

                276
            

            

                
            

            

                

            

        

            

                277
            

            

                
            

            

                
        // Determine the tau_mark first, the act_mark result is ignored.

            

        

            

                278
            

            

                1750
            

            

                
        let mut tau_mark = bitvec![u64, Lsb0; 0; lts.num_of_states()];

            

        

            

                279
            

            

                54729
            

            

                
        for s in lts.iter_states() {

            

        

            

                280
            

            

                54729
            

            

                
            tau_mark.set(*s, marked[*s][0]);

            

        

            

                281
            

            

                54729
            

            

                
        }

            

        

            

                282
            

            

                
            

            

                

            

        

            

                283
            

            

                
            

            

                
        // Determine the act_mark for every label that is not tau

            

        

            

                284
            

            

                1750
            

            

                
        let act_mark = (0..lts.labels().len())

            

        

            

                285
            

            

                15750
            

            

                
            .map(|label| {

            

        

            

                286
            

            

                15750
            

            

                
                let mut act_mark = bitvec![u64, Lsb0; 0; lts.num_of_states()];

            

        

            

                287
            

            

                
            

            

                

            

        

            

                288
            

            

                492561
            

            

                
                for s in lts.iter_states() {

            

        

            

                289
            

            

                492561
            

            

                
                    act_mark.set(*s, marked[*s][label]);

            

        

            

                290
            

            

                492561
            

            

                
                }

            

        

            

                291
            

            

                
            

            

                

            

        

            

                292
            

            

                15750
            

            

                
                compute_weak_act(

            

        

            

                293
            

            

                15750
            

            

                
                    &mut act_mark,

            

        

            

                294
            

            

                15750
            

            

                
                    &mut tau_mark,

            

        

            

                295
            

            

                15750
            

            

                
                    lts,

            

        

            

                296
            

            

                15750
            

            

                
                    blocks,

            

        

            

                297
            

            

                15750
            

            

                
                    incoming,

            

        

            

                298
            

            

                15750
            

            

                
                    block,

            

        

            

                299
            

            

                15750
            

            

                
                    LabelIndex::new(label),

            

        

            

                300
            

            

                
            

            

                
                );

            

        

            

                301
            

            

                15750
            

            

                
                act_mark

            

        

            

                302
            

            

                15750
            

            

                
            })

            

        

            

                303
            

            

                1750
            

            

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

            

        

            

                304
            

            

                
            

            

                

            

        

            

                305
            

            

                
            

            

                
        // Compute the markings using the optimised procedure.

            

        

            

                306
            

            

                1750
            

            

                
        compute_weak_acts_inner(marked, lts, incoming, blocks, block);

            

        

            

                307
            

            

                
            

            

                

            

        

            

                308
            

            

                
            

            

                
        // Check that the markings are the same for all labels, except tau

            

        

            

                309
            

            

                14000
            

            

                
        for label in 1..lts.labels().len() {

            

        

            

                310
            

            

                
            

            

                
            // The act_mark array starts at the first action, because we skip the tau action (index 0).

            

        

            

                311
            

            

                14000
            

            

                
            debug_assert!(

            

        

            

                312
            

            

                437832
            

            

                
                act_mark[label].iter().zip(marked.iter()).all(|(a, m)| a == m[label]),

            

        

            

                313
            

            

                
            

            

                
                "The act mark should be the same as the corresponding column in marked"

            

        

            

                314
            

            

                
            

            

                
            );

            

        

            

                315
            

            

                
            

            

                
        }

            

        

            

                316
            

            

                
            

            

                
    } else {

            

        

            

                317
            

            

                
            

            

                
        // No checking for correctness.

            

        

            

                318
            

            

                
            

            

                
        compute_weak_acts_inner(marked, lts, incoming, blocks, block);

            

        

            

                319
            

            

                
            

            

                
    }

            

        

            

                320
            

            

                1750
            

            

                
}

            

        

            

                321
            

            

                
            

            

                

            

        

            

                322
            

            

                
            

            

                
/// The inner implementation of [compute_weak_acts]. For all action a, sets s.marked[a] iff s =[a]> B, where B is the given block.

            

        

            

                323
            

            

                
            

            

                
///

            

        

            

                324
            

            

                
            

            

                
/// # Details

            

        

            

                325
            

            

                
            

            

                
///

            

        

            

                326
            

            

                
            

            

                
/// Requires that marked = 0 for all states.

            

        

            

                327
            

            

                1750
            

            

                
fn compute_weak_acts_inner<L: LTS>(

            

        

            

                328
            

            

                1750
            

            

                
    marked: &mut [BitArray],

            

        

            

                329
            

            

                1750
            

            

                
    lts: &L,

            

        

            

                330
            

            

                1750
            

            

                
    incoming: &IncomingTransitions<'_>,

            

        

            

                331
            

            

                1750
            

            

                
    blocks: &MarkedBlockPartition,

            

        

            

                332
            

            

                1750
            

            

                
    block: BlockIndex,

            

        

            

                333
            

            

                1750
            

            

                
) {

            

        

            

                334
            

            

                1750
            

            

                
    debug_assert!(

            

        

            

                335
            

            

                54729
            

            

                
        marked.iter().all(|m| m.not_any()),

            

        

            

                336
            

            

                
            

            

                
        "The marked array should be empty when calling compute_weak_acts_inner"

            

        

            

                337
            

            

                
            

            

                
    );

            

        

            

                338
            

            

                
            

            

                

            

        

            

                339
            

            

                
            

            

                
    // TODO: This should probably not be hardcoded.

            

        

            

                340
            

            

                1750
            

            

                
    let tau_index = LabelIndex::new(0);

            

        

            

                341
            

            

                1750
            

            

                
    debug_assert!(

            

        

            

                342
            

            

                1750
            

            

                
        lts.is_hidden_label(tau_index),

            

        

            

                343
            

            

                
            

            

                
        "The first label should be the tau action"

            

        

            

                344
            

            

                
            

            

                
    );

            

        

            

                345
            

            

                
            

            

                

            

        

            

                346
            

            

                
            

            

                
    // For t in B: t.marked[tau] := true

            

        

            

                347
            

            

                5230
            

            

                
    for t in blocks.iter_block(block) {

            

        

            

                348
            

            

                5230
            

            

                
        marked[t].set(*tau_index, true);

            

        

            

                349
            

            

                5230
            

            

                
    }

            

        

            

                350
            

            

                
            

            

                

            

        

            

                351
            

            

                54729
            

            

                
    for t in lts.iter_states() {

            

        

            

                352
            

            

                54729
            

            

                
        if marked[*t][*tau_index] {

            

        

            

                353
            

            

                
            

            

                
            // For each s -[tau]-> t do

            

        

            

                354
            

            

                6075
            

            

                
            for transition in incoming.incoming_silent_transitions(t) {

            

        

            

                355
            

            

                2853
            

            

                
                // s.marked[tau] := True if t.marked[tau]

            

        

            

                356
            

            

                2853
            

            

                
                marked[transition.from].set(*tau_index, true);

            

        

            

                357
            

            

                2853
            

            

                
            }

            

        

            

                358
            

            

                48654
            

            

                
        }

            

        

            

                359
            

            

                
            

            

                
    }

            

        

            

                360
            

            

                
            

            

                

            

        

            

                361
            

            

                54729
            

            

                
    for t in lts.iter_states() {

            

        

            

                362
            

            

                
            

            

                
        // For each t -[a]-> u do

            

        

            

                363
            

            

                151922
            

            

                
        for transition in lts.outgoing_transitions(t) {

            

        

            

                364
            

            

                
            

            

                
            // If u.marked[tau] then t.marked[a] := true

            

        

            

                365
            

            

                151922
            

            

                
            if marked[*transition.to][*tau_index] {

            

        

            

                366
            

            

                12339
            

            

                
                marked[*t].set(*transition.label, true);

            

        

            

                367
            

            

                139583
            

            

                
            }

            

        

            

                368
            

            

                
            

            

                
        }

            

        

            

                369
            

            

                
            

            

                

            

        

            

                370
            

            

                
            

            

                
        // For each s -[tau]-> t do

            

        

            

                371
            

            

                54729
            

            

                
        for transition in incoming.incoming_silent_transitions(t) {

            

        

            

                372
            

            

                
            

            

                
            // Computes s.marked[a] := s.marked[a] | t.marked[a] in place.

            

        

            

                373
            

            

                37043
            

            

                
            let [marked_s, marked_t] = marked

            

        

            

                374
            

            

                37043
            

            

                
                .get_disjoint_mut([*transition.from, *t])

            

        

            

                375
            

            

                37043
            

            

                
                .expect("The indices are disjoint");

            

        

            

                376
            

            

                37043
            

            

                
            for (i, number) in marked_s.as_raw_mut_slice().iter_mut().enumerate() {

            

        

            

                377
            

            

                37043
            

            

                
                *number |= marked_t.as_raw_slice()[i];

            

        

            

                378
            

            

                37043
            

            

                
            }

            

        

            

                379
            

            

                
            

            

                
        }

            

        

            

                380
            

            

                
            

            

                
    }

            

        

            

                381
            

            

                1750
            

            

                
}

            

        

            

                382
            

            

                
            

            

                

            

        

            

                383
            

            

                
            

            

                
/// Finding an action that can be used to perform a refinement step.

            

        

            

                384
            

            

                2548
            

            

                
fn find_act<L: LTS>(_lts: &L, blocks: &MarkedBlockPartition, marked: &mut [BitArray]) -> Option<LabelIndex> {

            

        

            

                385
            

            

                35532
            

            

                
    for block in (0..blocks.num_of_blocks()).map(BlockIndex::new) {

            

        

            

                386
            

            

                
            

            

                
        // Pick a representative state s from the block

            

        

            

                387
            

            

                35532
            

            

                
        let s = blocks.iter_block(block).next().expect("Block is non-empty");

            

        

            

                388
            

            

                68453
            

            

                
        for t in blocks.iter_block(block) {

            

        

            

                389
            

            

                68453
            

            

                
            if marked[s] != marked[t] {

            

        

            

                390
            

            

                
            

            

                
                // Find an action a such that s.marked[a] != t.marked[a]

            

        

            

                391
            

            

                5101
            

            

                
                for (label, marked_s) in marked[s].iter().enumerate() {

            

        

            

                392
            

            

                5101
            

            

                
                    if marked_s != marked[t][label] {

            

        

            

                393
            

            

                798
            

            

                
                        return Some(LabelIndex::new(label));

            

        

            

                394
            

            

                4303
            

            

                
                    }

            

        

            

                395
            

            

                
            

            

                
                }

            

        

            

                396
            

            

                67655
            

            

                
            }

            

        

            

                397
            

            

                
            

            

                
        }

            

        

            

                398
            

            

                
            

            

                
    }

            

        

            

                399
            

            

                
            

            

                

            

        

            

                400
            

            

                1750
            

            

                
    None

            

        

            

                401
            

            

                2548
            

            

                
}

            

        

            

                402
            

            

                
            

            

                

            

        

            

                403
            

            

                
            

            

                
/// Splits the given block according to the given marking.

            

        

            

                404
            

            

                3464876
            

            

                
fn stabilise(block: BlockIndex, act_mark: &mut BitArray, blocks: &mut MarkedBlockPartition) {

            

        

            

                405
            

            

                12265245
            

            

                
    blocks.split_block(block, |state| act_mark[*state]);

            

        

            

                406
            

            

                3464876
            

            

                
}

            

        

            

                407
            

            

                
            

            

                

            

        

            

                408
            

            

                
            

            

                
/// Splits the given block according to the given marking.

            

        

            

                409
            

            

                9774
            

            

                
fn stabilise_act(block: BlockIndex, act: LabelIndex, marked: &mut [BitArray], blocks: &mut MarkedBlockPartition) {

            

        

            

                410
            

            

                29279
            

            

                
    blocks.split_block(block, |state| marked[*state][*act]);

            

        

            

                411
            

            

                9774
            

            

                
}

            

        

            

                412
            

            

                
            

            

                

            

        

            

                413
            

            

                
            

            

                
#[cfg(test)]

            

        

            

                414
            

            

                
            

            

                
mod tests {

            

        

            

                415
            

            

                
            

            

                
    use merc_io::DumpFiles;

            

        

            

                416
            

            

                
            

            

                
    use merc_lts::LTS;

            

        

            

                417
            

            

                
            

            

                
    use merc_lts::random_lts;

            

        

            

                418
            

            

                
            

            

                
    use merc_lts::write_aut;

            

        

            

                419
            

            

                
            

            

                
    use merc_utilities::Timing;

            

        

            

                420
            

            

                
            

            

                
    use merc_utilities::random_test;

            

        

            

                421
            

            

                
            

            

                

            

        

            

                422
            

            

                
            

            

                
    use crate::Equivalence;

            

        

            

                423
            

            

                
            

            

                
    use crate::compare_lts;

            

        

            

                424
            

            

                
            

            

                
    use crate::reduce_lts;

            

        

            

                425
            

            

                
            

            

                

            

        

            

                426
            

            

                
            

            

                
    #[test]

            

        

            

                427
            

            

                
            

            

                
    #[cfg_attr(miri, ignore)]

            

        

            

                428
            

            

                1
            

            

                
    fn test_weak_bisimulation() {

            

        

            

                429
            

            

                100
            

            

                
        random_test(100, |rng| {

            

        

            

                430
            

            

                100
            

            

                
            let mut files = DumpFiles::new("test_weak_bisimulation");

            

        

            

                431
            

            

                
            

            

                

            

        

            

                432
            

            

                100
            

            

                
            let lts = random_lts(rng, 100, 10, 3);

            

        

            

                433
            

            

                100
            

            

                
            let mut timing = Timing::new();

            

        

            

                434
            

            

                100
            

            

                
            files.dump("input.aut", |f| write_aut(f, &lts)).unwrap();

            

        

            

                435
            

            

                
            

            

                

            

        

            

                436
            

            

                100
            

            

                
            let result = reduce_lts(lts.clone(), Equivalence::WeakBisim, false, &mut timing);

            

        

            

                437
            

            

                100
            

            

                
            let expected = reduce_lts(lts, Equivalence::WeakBisimSigref, false, &mut timing);

            

        

            

                438
            

            

                
            

            

                

            

        

            

                439
            

            

                100
            

            

                
            assert_eq!(result.num_of_states(), expected.num_of_states());

            

        

            

                440
            

            

                100
            

            

                
            assert_eq!(result.num_of_transitions(), expected.num_of_transitions());

            

        

            

                441
            

            

                
            

            

                

            

        

            

                442
            

            

                100
            

            

                
            files.dump("result.aut", |f| write_aut(f, &result)).unwrap();

            

        

            

                443
            

            

                100
            

            

                
            files.dump("expected.aut", |f| write_aut(f, &expected)).unwrap();

            

        

            

                444
            

            

                
            

            

                

            

        

            

                445
            

            

                100
            

            

                
            assert!(compare_lts(

            

        

            

                446
            

            

                100
            

            

                
                Equivalence::StrongBisim,

            

        

            

                447
            

            

                100
            

            

                
                result,

            

        

            

                448
            

            

                100
            

            

                
                expected,

            

        

            

                449
            

            

                
            

            

                
                false,

            

        

            

                450
            

            

                100
            

            

                
                &mut timing

            

        

            

                451
            

            

                
            

            

                
            ));

            

        

            

                452
            

            

                100
            

            

                
        })

            

        

            

                453
            

            

                1
            

            

                
    }

            

        

            

                454
            

            

                
            

            

                

            

        

            

                455
            

            

                
            

            

                
    #[test]

            

        

            

                456
            

            

                
            

            

                
    #[cfg_attr(miri, ignore)]

            

        

            

                457
            

            

                1
            

            

                
    fn test_weak_bisimulation_parallel() {

            

        

            

                458
            

            

                100
            

            

                
        random_test(100, |rng| {

            

        

            

                459
            

            

                100
            

            

                
            let mut files = DumpFiles::new("test_weak_bisimulation_parallel");

            

        

            

                460
            

            

                
            

            

                

            

        

            

                461
            

            

                100
            

            

                
            let lts = random_lts(rng, 10, 10, 3);

            

        

            

                462
            

            

                100
            

            

                
            let mut timing = Timing::new();

            

        

            

                463
            

            

                100
            

            

                
            files.dump("input.aut", |f| write_aut(f, &lts)).unwrap();

            

        

            

                464
            

            

                
            

            

                

            

        

            

                465
            

            

                100
            

            

                
            let result = reduce_lts(lts.clone(), Equivalence::WeakBisim, false, &mut timing);

            

        

            

                466
            

            

                100
            

            

                
            let expected = reduce_lts(lts, Equivalence::WeakBisimParallel, false, &mut timing);

            

        

            

                467
            

            

                
            

            

                

            

        

            

                468
            

            

                100
            

            

                
            assert_eq!(result.num_of_states(), expected.num_of_states());

            

        

            

                469
            

            

                100
            

            

                
            assert_eq!(result.num_of_transitions(), expected.num_of_transitions());

            

        

            

                470
            

            

                
            

            

                

            

        

            

                471
            

            

                100
            

            

                
            files.dump("result.aut", |f| write_aut(f, &result)).unwrap();

            

        

            

                472
            

            

                100
            

            

                
            files.dump("expected.aut", |f| write_aut(f, &expected)).unwrap();

            

        

            

                473
            

            

                
            

            

                

            

        

            

                474
            

            

                100
            

            

                
            assert!(compare_lts(

            

        

            

                475
            

            

                100
            

            

                
                Equivalence::StrongBisim,

            

        

            

                476
            

            

                100
            

            

                
                result,

            

        

            

                477
            

            

                100
            

            

                
                expected,

            

        

            

                478
            

            

                
            

            

                
                false,

            

        

            

                479
            

            

                100
            

            

                
                &mut timing

            

        

            

                480
            

            

                
            

            

                
            ));

            

        

            

                481
            

            

                100
            

            

                
        })

            

        

            

                482
            

            

                1
            

            

                
    }

            

        

            

                483
            

            

                
            

            

                
}