Grcov report - combine.rs

1

use log::info;

2

use merc_collections::IndexedSet;

3

use merc_collections::SetIndex;

4

use merc_collections::VecBag;

5

use merc_io::TimeProgress;

6

use merc_lts::LTS;

7

use merc_lts::LabelIndex;

8

use merc_lts::LtsAction;

9

use merc_lts::LtsBuilder;

10

use merc_lts::LtsMultiAction;

11

use merc_lts::SimpleAction;

12

use merc_lts::StateIndex;

13

use merc_lts::Transition;

14

use merc_lts::TransitionLabel;

15

use merc_syntax::CommExpr;

16

use merc_syntax::MultiActionLabel;

17

use merc_utilities::MercError;

18

use merc_utilities::Timing;

19

use streaming_iterator::StreamingIterator;

20

21

/// The trait for labels used in the composition operator.

22

pub trait CombineLabel: TransitionLabel + Ord {

23

    /// Returns true iff the data arguments of two actions are compatible for communication.

24

    /// Defaults to `true` for label types without structured arguments (e.g., `String`).

25

    fn comm_args_compatible(&self, _other: &Self) -> bool {

26

        true

27

28

29

    /// Creates a new action as the result of a communication expression with the given `label`.

30

    /// `representative` is one of the matched input actions and provides argument values.

31

    fn from_comm(label: String, representative: &Self) -> Self;

32

33

34

impl CombineLabel for SimpleAction {

35

    fn comm_args_compatible(&self, other: &Self) -> bool {

36

        self.arguments() == other.arguments()

37

38

39

    fn from_comm(label: String, representative: &Self) -> Self {

40

        SimpleAction::new(label, representative.arguments().to_vec())

41

42

43

44

impl CombineLabel for LtsAction {

45

    fn comm_args_compatible(&self, other: &Self) -> bool {

46

        self.arguments() == other.arguments()

47

48

49

    fn from_comm(label: String, representative: &Self) -> Self {

50

        LtsAction::new(label, representative.arguments().to_vec())

51

52

53

54

/// Computes the parallel composition hide(allow(comm(L1 || ... || Ln))).

55

///

56

/// The `builder` is used to construct the resulting LTS, which can also be

57

/// stored immediately in a file.

58

///

59

/// We interpret empty hide, allow and comm sets as the operator not being present.

60

pub fn combine_lts<L: LTS<Label = LtsMultiAction<A>>, A: CombineLabel, B: LtsBuilder<L::Label>>(

61

    builder: &mut B,

62

    parallel_composition: Vec<L>,

63

    hide: &[String],

64

    allow: &[MultiActionLabel],

65

    comm: &[CommExpr],

66

    timing: &Timing,

67

) -> Result<(), MercError> {

68

    if parallel_composition.is_empty() {

69

        return Err("At least one LTS is required for composition.".into());

70

71

72

    if allow.iter().any(|allow| allow.is_tau_label()) {

73

        return Err("Allow set cannot contain the tau action.".into());

74

75

76

    if comm.iter().any(|comm| comm.from.is_tau_label()) {

77

        return Err("Communication expressions cannot have tau actions on the left-hand side.".into());

78

79

80

    for (i, comm_i) in comm.iter().enumerate() {

81

        if comm_i.from.actions.len() < 2 {

82

            return Err(format!(

83

                "Communication expressions must have at least two actions on the left-hand side, but {comm_i} does not."

84

85

            .into());

86

87

88

        // The left hand side of a communication cannot overlap with any other communication's left hand side.

89

        for (j, comm_j) in comm.iter().enumerate() {

90

            if i != j && comm_i.from.actions.iter().any(|a| comm_j.from.actions.contains(a)) {

91

                return Err(format!(

92

                    "Communication expressions cannot have overlapping left-hand sides, i.e. {comm_i} and {comm_j}."

93

94

                .into());

95

96

97

98

        // The right hand side of a communication cannot be in another communication's left hand side.

99

        for (j, comm_j) in comm.iter().enumerate() {

100

            if i != j && comm_j.from.actions.contains(&comm_i.to) {

101

                return Err(

102

                    format!("Communication expressions cannot have right-hand side in another communication's left-hand side, i.e. {comm_i} and {comm_j}.").into(),

103

);

104

105

106

107

108

    // Keep track of the discovered states in the combined LTS.

109

    let mut discovered: IndexedSet<Vec<StateIndex>> = IndexedSet::new();

110

    let (index, _) = discovered.insert(

111

        parallel_composition

112

            .iter()

113

            .map(|lts| lts.initial_state_index())

114

            .collect(),

115

);

116

117

    let progress = TimeProgress::new(

118

        |(states, transitions): (usize, usize)| {

119

            info!("Explored {states} states, {transitions} transitions...");

120

},

121

1,

122

);

123

124

    // Pre-sort the allow set for efficient matching.

125

    let sorted_allow: Vec<SortedMultiActionLabel> = allow.iter().map(SortedMultiActionLabel::new).collect();

126

127

    // Working refers to the state vectors in discovered.

128

    let mut working: Vec<SetIndex> = vec![index];

129

    timing.measure("compose", || -> Result<(), MercError> {

130

        while let Some(current) = working.pop() {

131

            // Clone the current state vector since discovered may be mutated below.

132

            let current_state_vector = discovered

133

                .get(current)

134

                .expect("State must be in the discovered set")

135

                .as_ref();

136

137

            // Loop over all subsets of LTSs and their outgoing transitions in the current state vector.

138

            let mut iter = ParallelTransitionIter::new(&parallel_composition, current_state_vector);

139

            loop {

140

                iter.advance();

141

                let Some(transition) = iter.get() else {

142

                    break;

143

};

144

145

                // Build the combined multi-action alpha = alpha_{j_0} | ... | alpha_{j_m}.

146

                let mut actions = VecBag::new();

147

                for (k, &lts_idx) in transition.subset_indices.iter().enumerate() {

148

                    let label_idx = transition.labels[k];

149

                    let label = &parallel_composition[lts_idx].labels()[label_idx];

150

                    for action in label.actions() {

151

                        actions.insert(action.clone());

152

153

154

                let multi_action = LtsMultiAction::new(actions);

155

156

                // Apply communication: alpha = gamma_C(alpha).

157

                let multi_action = communicate(comm, multi_action);

158

159

                // Check allow: alpha in A ∪ {tau}.

160

                if !is_allowed(&sorted_allow, &SortedLtsMultiAction::new(&multi_action)) {

161

                    continue;

162

163

164

                // Apply hide: alpha = tau_I(alpha).

165

                let multi_action = hide_action(hide, multi_action);

166

167

                // Copy the target before advancing invalidates it.

168

                let target_vec = transition.target.to_vec();

169

170

                let (target_index, is_new) = discovered.insert(target_vec);

171

                let to = StateIndex::new(*target_index);

172

                builder.add_transition(StateIndex::new(*current), &multi_action, to)?;

173

174

                if is_new {

175

                    working.push(target_index);

176

177

178

179

            progress.print((discovered.len(), builder.num_of_transitions()));

180

181

182

        Ok(())

183

    })?;

184

185

    info!(

186

        "Composition complete: {} states, {} transitions",

187

        discovered.len(),

188

        builder.num_of_transitions()

189

);

190

191

    builder.finish(StateIndex::new(*index))?;

192

    Ok(())

193

194

195

/// Applies the communication operator to a multi-action according to the given

196

/// communication expressions.

197

///

198

/// # Details

199

/// Applies the communication operator $\gamma_C$ to a multi-action.

200

///

201

/// For each communication expression $a_1 | \cdots | a_n \rightarrow c$ in $C$,

202

/// repeatedly finds matching sub-multisets of actions (with equal arguments)

203

/// and replaces them with the result action $c$.

204

fn communicate<L: CombineLabel>(comm: &[CommExpr], action: LtsMultiAction<L>) -> LtsMultiAction<L> {

205

    let mut actions = action.into_actions().to_vec();

206

207

    for expr in comm {

208

        // Try to find a matching sub-multiset for this communication expression.

209

        while let Some(replacement) = find_communication_match(&actions, expr) {

210

            actions = replacement;

211

212

213

214

    LtsMultiAction::new(VecBag::from_vec(actions))

215

216

217

/// Tries to find actions matching a single communication expression

218

/// $a_1 | \cdots | a_n \rightarrow c$ within the given action list.

219

///

220

/// Returns the resulting action list with the matched actions replaced by the

221

/// communicated action, or `None` if no match was found.

222

fn find_communication_match<L: CombineLabel>(actions: &[L], expr: &CommExpr) -> Option<Vec<L>> {

223

    // For each action name in the communication expression's left-hand side,

224

    // find a matching action with the same label. All matched actions must

225

    // have the same arguments.

226

    let mut matched_indices = Vec::new();

227

    let mut first_match: Option<usize> = None;

228

229

    for required_name in &expr.from.actions {

230

        let mut found = false;

231

        for (i, action) in actions.iter().enumerate() {

232

            if matched_indices.contains(&i) {

233

                continue;

234

235

            if action.matches_label(required_name) {

236

                // All matched actions must share the same arguments.

237

                if let Some(first) = first_match {

238

                    if !action.comm_args_compatible(&actions[first]) {

239

                        continue;

240

241

                } else {

242

                    first_match = Some(i);

243

244

                matched_indices.push(i);

245

                found = true;

246

                break;

247

248

249

        if !found {

250

            return None;

251

252

253

254

    // Build the result: remove matched actions and add the communicated action.

255

    let mut result: Vec<L> = actions

256

        .iter()

257

        .enumerate()

258

        .filter(|(i, _)| !matched_indices.contains(i))

259

        .map(|(_, a)| a.clone())

260

        .collect();

261

262

    let representative = &actions[first_match.expect("first_match is always Some when all actions are matched")];

263

    result.push(L::from_comm(expr.to.clone(), representative));

264

    Some(result)

265

266

267

/// Returns true iff the given multi-action is allowed by the allow operator.

268

///

269

/// A multi-action is allowed if:

270

/// - The action is tau (always allowed), or

271

/// - The action label names, compared as sorted multisets, match one of the

272

///   entries in the allow set.

273

fn is_allowed<L: CombineLabel>(allow: &[SortedMultiActionLabel], action: &SortedLtsMultiAction<L>) -> bool {

274

    if action.is_tau_label() {

275

        return true;

276

277

278

    allow.iter().any(|allowed| {

279

        allowed.actions.len() == action.len()

280

            && allowed

281

                .actions

282

                .iter()

283

                .zip(action.iter_actions())

284

                .all(|(name, a)| a.matches_label(name))

285

})

286

287

288

/// Applies the hide operator $\tau_I$ to a multi-action.

289

///

290

/// Removes all actions whose label is in the hide set $I$. If all actions are

291

/// hidden the result is the tau action (empty multi-action).

292

fn hide_action<L: CombineLabel>(hide: &[String], mut action: LtsMultiAction<L>) -> LtsMultiAction<L> {

293

    if !hide.is_empty() {

294

        action.retain(|a| !hide.iter().any(|h| a.matches_label(h)));

295

296

    action

297

298

299

/// A streaming iterator over the Cartesian product of sequences with given

300

/// lengths.

301

///

302

/// Each call to `advance` updates an internal index buffer (odometer) that

303

/// represents one element of the Cartesian product. The buffer is reused

304

/// across calls to avoid allocation. The yielded `&[usize]` contains the

305

/// current index into each factor.

306

pub struct CartesianProduct {

307

    /// The length of each factor.

308

    lengths: Vec<usize>,

309

    /// Current index into each factor (odometer).

310

    indices: Vec<usize>,

311

312

    done: bool,

313

    started: bool,

314

315

316

impl CartesianProduct {

317

    /// Creates a new Cartesian product iterator for factors with the given

318

    /// lengths.

319

///

320

    /// If any length is zero the iterator will yield no elements.

321

    pub fn new(lengths: Vec<usize>) -> Self {

322

        let done = lengths.contains(&0);

323

        let n = lengths.len();

324

        CartesianProduct {

325

            lengths,

326

            indices: vec![0; n],

327

            done,

328

            started: false,

329

330

331

332

    /// Returns `true` if a next combination exists, `false` if exhausted.

333

    fn advance_impl(&mut self) -> bool {

334

        for i in (0..self.indices.len()).rev() {

335

            self.indices[i] += 1;

336

            if self.indices[i] < self.lengths[i] {

337

                return true;

338

339

            self.indices[i] = 0;

340

341

        false

342

343

344

345

impl StreamingIterator for CartesianProduct {

346

    type Item = [usize];

347

348

    fn advance(&mut self) {

349

        if self.done {

350

            return;

351

352

353

        if self.started {

354

            if !self.advance_impl() {

355

                self.done = true;

356

357

        } else {

358

            self.started = true;

359

360

361

362

    fn get(&self) -> Option<&Self::Item> {

363

        if self.done || !self.started {

364

            None

365

        } else {

366

            Some(&self.indices)

367

368

369

370

371

/// A multi-action label with action names sorted, for proper multiset

372

/// comparison with [`SortedLtsMultiAction`].

373

struct SortedMultiActionLabel {

374

    /// Action names in sorted order.

375

    actions: Vec<String>,

376

377

378

impl SortedMultiActionLabel {

379

    fn new(label: &MultiActionLabel) -> Self {

380

        let mut actions = label.actions.clone();

381

        actions.sort();

382

        SortedMultiActionLabel { actions }

383

384

385

386

/// A view of an [`LtsMultiAction`] for multiset comparison with [`SortedMultiActionLabel`].

387

///

388

/// Since `VecBag<L>` iterates in sorted order, the actions are already in

389

/// non-decreasing order, so no additional sorting is needed here.

390

struct SortedLtsMultiAction<'a, L: Ord> {

391

    action: &'a LtsMultiAction<L>,

392

393

394

impl<'a, L: TransitionLabel> SortedLtsMultiAction<'a, L> {

395

    fn new(action: &'a LtsMultiAction<L>) -> Self {

396

        SortedLtsMultiAction { action }

397

398

399

    fn is_tau_label(&self) -> bool {

400

        self.action.is_tau_label()

401

402

403

    fn iter_actions(&self) -> impl Iterator<Item = &L> {

404

        self.action.actions().iter()

405

406

407

    fn len(&self) -> usize {

408

        self.action.actions().len()

409

410

411

412

/// The output of a parallel transition step: label indices from participating

413

/// LTSs and the combined target state vector.

414

pub struct ParallelTransition {

415

    /// Indices of LTSs participating in this transition's subset.

416

    pub subset_indices: Vec<usize>,

417

    /// Label indices from each participating LTS in the current subset.

418

    pub labels: Vec<LabelIndex>,

419

    /// Target state vector: for LTSs in the subset, the transition target;

420

    /// for others, the current state is retained.

421

    pub target: Vec<StateIndex>,

422

423

424

/// A streaming iterator that lazily enumerates all parallel transitions from a

425

/// given state vector across multiple LTSs.

426

///

427

/// For each non-empty subset $J \subseteq \{0, \ldots, n-1\}$ of LTSs,

428

/// enumerates the Cartesian product of outgoing transitions from the LTSs in

429

/// $J$. The result buffers are updated in-place to avoid per-`next()` allocation.

430

pub struct ParallelTransitionIter {

431

    /// Pre-collected outgoing transitions for each LTS at the current state.

432

    all_outgoing: Vec<Vec<Transition>>,

433

434

    /// Current subset bitmask (1 to 2^n - 1).

435

    current_subset: usize,

436

    /// Upper bound for subset enumeration (2^n).

437

    max_subset: usize,

438

439

    /// Indices of LTSs participating in the current subset.

440

    subset_indices: Vec<usize>,

441

    /// The Cartesian product iterator for the current subset.

442

    product: CartesianProduct,

443

444

    /// The base target state vector (the current state for each LTS).

445

    base_target: Vec<StateIndex>,

446

    /// Output buffer, reused across `advance()` calls.

447

    result: ParallelTransition,

448

449

    done: bool,

450

    started: bool,

451

452

453

impl ParallelTransitionIter {

454

    /// Creates a new iterator over parallel transitions for the given LTSs

455

    /// and current state vector.

456

    pub fn new<L: LTS>(lts_list: &[L], current_states: &[StateIndex]) -> Self {

457

        assert!(

458

            lts_list.len() < usize::BITS as usize,

459

            "Number of LTSs exceeds maximum supported for subset enumeration"

460

);

461

462

        let all_outgoing: Vec<Vec<Transition>> = lts_list

463

            .iter()

464

            .zip(current_states.iter())

465

            .map(|(lts, &state)| lts.outgoing_transitions(state).collect())

466

            .collect();

467

468

        ParallelTransitionIter {

469

            all_outgoing,

470

            current_subset: 1,

471

            max_subset: 1usize << lts_list.len(),

472

            subset_indices: Vec::new(),

473

            product: CartesianProduct::new(vec![]),

474

            base_target: current_states.to_vec(),

475

            result: ParallelTransition {

476

                subset_indices: Vec::new(),

477

                labels: Vec::new(),

478

                target: current_states.to_vec(),

479

},

480

            done: false,

481

            started: false,

482

483

484

485

    /// Builds a `CartesianProduct` for the current subset bitmask.

486

    /// Returns `true` if the subset produces a non-empty Cartesian product.

487

    fn setup_subset(&mut self) -> bool {

488

        self.subset_indices.clear();

489

490

        let mut lengths = Vec::new();

491

        for i in 0..self.all_outgoing.len() {

492

            if self.current_subset & (1 << i) != 0 {

493

                if self.all_outgoing[i].is_empty() {

494

                    return false;

495

496

                self.subset_indices.push(i);

497

                lengths.push(self.all_outgoing[i].len());

498

499

500

501

        self.product = CartesianProduct::new(lengths);

502

        true

503

504

505

    /// Fills the result buffer from the product's current indices.

506

    fn fill_result(&mut self) {

507

        self.result.subset_indices.clear();

508

        self.result.subset_indices.extend_from_slice(&self.subset_indices);

509

        self.result.labels.clear();

510

        self.result.target.copy_from_slice(&self.base_target);

511

512

        for (k, &lts_idx) in self.subset_indices.iter().enumerate() {

513

            let transition = &self.all_outgoing[lts_idx][self.product.indices[k]];

514

            self.result.labels.push(transition.label);

515

            self.result.target[lts_idx] = transition.to;

516

517

518

519

520

impl StreamingIterator for ParallelTransitionIter {

521

    type Item = ParallelTransition;

522

523

    fn advance(&mut self) {

524

        if self.done {

525

            return;

526

527

528

        // Try to advance within current Cartesian product.

529

        if self.started {

530

            self.product.advance();

531

            if self.product.get().is_some() {

532

                self.fill_result();

533

                return;

534

535

            self.current_subset += 1;

536

537

        self.started = true;

538

539

        // Find next subset with a non-empty Cartesian product.

540

        while self.current_subset < self.max_subset {

541

            if self.setup_subset() {

542

                self.product.advance();

543

                if self.product.get().is_some() {

544

                    self.fill_result();

545

                    return;

546

547

548

            self.current_subset += 1;

549

550

551

        self.done = true;

552

553

554

    fn get(&self) -> Option<&Self::Item> {

555

        if self.done || !self.started {

556

            None

557

        } else {

558

            Some(&self.result)

559

560

561

562

563

#[cfg(test)]

564

mod tests {

565

    use std::fs::File;

566

    use std::io::Write;

567

    use std::io::{self};

568

    use std::path::Path;

569

    use std::process::Command;

570

571

    use itertools::Itertools;

572

    use log::info;

573

    use log::trace;

574

    use merc_collections::VecBag;

575

    use merc_lts::LTS;

576

    use merc_lts::LtsAction;

577

    use merc_lts::LtsBuilderFast;

578

    use merc_lts::LtsMultiAction;

579

    use merc_lts::StateIndex;

580

    use merc_lts::TransitionLabel;

581

    use merc_lts::random_lts;

582

    use merc_lts::read_lts;

583

    use merc_lts::write_mcrl2_aut;

584

    use merc_reduction::Equivalence;

585

    use merc_reduction::compare_lts;

586

    use merc_syntax::CommExpr;

587

    use merc_syntax::MultiActionLabel;

588

    use merc_utilities::MercError;

589

    use merc_utilities::Timing;

590

    use merc_utilities::random_test;

591

    use rand::RngExt;

592

    use rand::seq::IndexedRandom;

593

    use rand::seq::IteratorRandom;

594

    use tempfile::TempDir;

595

596

    use crate::combine::combine_lts;

597

598

    /// Uses `MERC_DUMP` as the temporary directory if set, and otherwise the default temp directory.

599

    fn temp_dir(name: &str) -> Result<TempDir, MercError> {

600

        if let Ok(dump_dir) = std::env::var("MERC_DUMP") {

601

            // Check if the directory is an absolute path

602

            if !Path::new(dump_dir.as_str()).is_absolute() {

603

                panic!("MERC_DUMP must be an absolute path, because tests write relative to their source file.");

604

605

606

            // If we are asking for MERC_DUMP, disable cleanup.

607

            let mut dir = tempfile::TempDir::with_prefix_in(name, dump_dir)?;

608

            dir.disable_cleanup(true);

609

            Ok(dir)

610

        } else {

611

            tempfile::tempdir().map_err(|e| e.into())

612

613

614

615

    fn traced_status(command: &mut Command) -> io::Result<std::process::ExitStatus> {

616

        trace!(

617

            "{} {}",

618

            command.get_program().to_string_lossy(),

619

            command

620

                .get_args()

621

                .map(|arg| arg.to_string_lossy())

622

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

623

                .join(" ")

624

);

625

        command.status()

626

627

628

    /// Returns a random multi-action label with action names sampled from the given list.

629

    fn random_multi_action<R: rand::Rng>(rng: &mut R, actions: &[String], max_size: usize) -> MultiActionLabel {

630

        let max_size = usize::min(actions.len(), max_size);

631

        let size = rng.random_range(0..=max_size);

632

        let selected_actions = actions.sample(rng, size).cloned().collect::<Vec<_>>();

633

        MultiActionLabel::new(selected_actions)

634

635

636

    #[test]

637

1

    fn test_mcrl2_ltscombine() {

638

1

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

639

1

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

640

1

            return;

641

};

642

643

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

644

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

645

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

646

647

        // Write the random LTS to a temp file for ltsconvert to process.

648

        let temp_dir = temp_dir("test_mcrl2_ltscombine").unwrap();

649

650

        let spec_path = temp_dir.path().join("spec.mcrl2");

651

        let lps_path = temp_dir.path().join("spec.lps");

652

        let output_path = temp_dir.path().join("output.lts");

653

654

        // Generate a dummy linear process specification to convert the .aut files to .lts format.

655

        writeln!(&mut File::create(&spec_path).unwrap(), "act a, b, c; init delta;").unwrap();

656

657

        let status = traced_status(Command::new(&mcrl2_mcrl22lps).arg(&spec_path).arg(&lps_path))

658

            .expect("Failed to run ltsconvert");

659

        assert!(status.success(), "ltsconvert failed with status: {status}");

660

661

        random_test(100, |rng| {

662

            let left_lts = random_lts::<String, _>(rng, 1000, 3)

663

                .relabel(|label| Ok(LtsMultiAction::new(VecBag::singleton(LtsAction::new(label, vec![])))))

664

                .unwrap();

665

            let right_lts = random_lts::<String, _>(rng, 1000, 3)

666

                .relabel(|label| Ok(LtsMultiAction::new(VecBag::singleton(LtsAction::new(label, vec![])))))

667

                .unwrap();

668

669

            let left_path = temp_dir.path().join("left.aut");

670

            let right_path = temp_dir.path().join("right.aut");

671

            write_mcrl2_aut(&mut File::create(&left_path).unwrap(), &left_lts).unwrap();

672

            write_mcrl2_aut(&mut File::create(&right_path).unwrap(), &right_lts).unwrap();

673

674

            // For mCRL2's ltscombine we need to convert the inputs to the mCRL2 LTS format.

675

            let left_lts_path = temp_dir.path().join("left.lts");

676

            let right_lts_path = temp_dir.path().join("right.lts");

677

            let status = traced_status(

678

                Command::new(&mcrl2_ltsconvert)

679

                    .arg("-enone")

680

                    .arg(&left_path)

681

                    .arg(&left_lts_path)

682

                    .arg("-l")

683

                    .arg(&lps_path),

684

685

            .expect("Failed to run ltsconvert");

686

            assert!(status.success(), "ltsconvert failed with status: {status}");

687

688

            let status = traced_status(

689

                Command::new(&mcrl2_ltsconvert)

690

                    .arg("-enone")

691

                    .arg(&right_path)

692

                    .arg(&right_lts_path)

693

                    .arg("-l")

694

                    .arg(&lps_path),

695

696

            .expect("Failed to run ltsconvert");

697

            assert!(status.success(), "ltsconvert failed with status: {status}");

698

699

            // Allow an arbitrary subset of labels

700

            let labels = left_lts

701

                .labels()

702

                .iter()

703

                .chain(right_lts.labels().iter())

704

                .map(|l| l.to_string())

705

                .filter(|label| !label.is_tau_label())

706

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

707

708

            let num_of_allowed = rng.random_range(0..=labels.len());

709

            let allow = (0..num_of_allowed)

710

                .map(|_| random_multi_action(rng, &labels, 3))

711

                .filter(|a| !a.is_tau_label())

712

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

713

714

            let num_of_hidden = rng.random_range(0..=labels.len());

715

            let hide = labels

716

                .iter()

717

                .cloned()

718

                .filter(|a| !a.is_tau_label())

719

                .sample(rng, num_of_hidden);

720

721

            let num_of_comm = rng.random_range(0..=5);

722

            let mut comm = (0..num_of_comm)

723

                .map(|_| {

724

                    let size = rng.random_range(2..=3);

725

                    let actions = random_multi_action(rng, &labels, size);

726

                    let to = labels.choose(rng).unwrap().clone();

727

                    CommExpr::new(actions, to)

728

})

729

                .filter(|comm| {

730

                    !comm.from.is_tau_label() && comm.from.actions.contains(&comm.to) && comm.from.actions.len() >= 2

731

})

732

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

733

734

            comm.sort_unstable();

735

            comm.dedup();

736

737

            // Remove communication expressions with overlapping left-hand sides.

738

            let comm = comm

739

                .iter()

740

                .filter(|&comm_i| {

741

                    !comm.iter().any(|comm_j| {

742

                        comm_i != comm_j && comm_i.from.actions.iter().any(|a| comm_j.from.actions.contains(a))

743

})

744

})

745

                .cloned()

746

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

747

748

            info!("Allow set {{{}}}", allow.iter().format(", "));

749

            info!("Hide set {{{}}}", hide.iter().format(", "));

750

            info!("Comm set {{{}}}", comm.iter().format(", "));

751

752

            // Use ltscombine to compute the combined LTS, which we will compare against our implementation's result

753

            let mut command = Command::new(&mcrl2_ltscombine);

754

            command.arg(&left_lts_path).arg(&right_lts_path);

755

            if !allow.is_empty() {

756

                command.arg(format!("--allow={{{}}}", allow.iter().format(", ")));

757

758

            if !hide.is_empty() {

759

                command.arg(format!("--hide={{{}}}", hide.iter().format(", ")));

760

761

            if !comm.is_empty() {

762

                command.arg(format!("--comm={{{}}}", comm.iter().format(", ")));

763

764

            command.arg(&output_path);

765

766

            let status = traced_status(&mut command).expect("Failed to run ltscombine");

767

            assert!(status.success(), "ltscombine failed with status: {status}");

768

769

            let expected_lts = read_lts(&File::open(&output_path).unwrap(), false).unwrap();

770

            let expected_path = temp_dir.path().join("expected.aut");

771

            write_mcrl2_aut(&mut File::create(&expected_path).unwrap(), &expected_lts).unwrap();

772

773

            let mut result: LtsBuilderFast<LtsMultiAction<LtsAction>> = LtsBuilderFast::new(Vec::new(), Vec::new());

774

            combine_lts(

775

                &mut result,

776

                vec![left_lts, right_lts],

777

                &hide,

778

                &allow,

779

                &comm,

780

                &mut Timing::new(),

781

782

            .unwrap();

783

            let result_lts = result.finish(StateIndex::new(0), false);

784

785

            let result_path = temp_dir.path().join("result.aut");

786

            write_mcrl2_aut(&mut File::create(&result_path).unwrap(), &result_lts).unwrap();

787

788

            assert!(

789

                compare_lts(

790

                    Equivalence::StrongBisim,

791

                    expected_lts,

792

                    result_lts,

793

                    false,

794

                    &mut Timing::new(),

795

),

796

                "The resulting LTSs are not bisimilar."

797

);

798

});

799

1

800