mCRL2
Loading...
Searching...
No Matches
liblts_bisim_gjkw.cpp File Reference

O(m log n)-time stuttering equivalence algorithm. More...

Go to the source code of this file.

Classes

class  mcrl2::lts::detail::constln_ptr_less
 function object to compare two constln_t pointers based on their contents More...
 

Namespaces

namespace  mcrl2
 A class that takes a linear process specification and checks all tau-summands of that LPS for confluence.
 
namespace  mcrl2::lts
 The main LTS namespace.
 
namespace  mcrl2::lts::detail
 A base class for the lts_dot labelled transition system.
 
namespace  mcrl2::lts::detail::bisim_gjkw
 

Macros

#define PARANOID_CHECK
 

Typedefs

typedef std::set< bisim_gjkw::constln_t *, constln_ptr_lessmcrl2::lts::detail::R_map_t
 

Functions

static void mcrl2::lts::detail::bisim_gjkw::blue_is_smaller (block_t *BlueB, block_t *RedB, const constln_t *NewC)
 moves temporary counters to normal ones if the blue block is smaller
 
static void mcrl2::lts::detail::bisim_gjkw::red_is_smaller (block_t *BlueB, block_t *RedB)
 moves temporary counters to normal ones if the red block is smaller
 

Detailed Description

O(m log n)-time stuttering equivalence algorithm.

This file implements the efficient partition refinement algorithm by Groote / Jansen / Keiren / Wijs to calculate the stuttering equivalence quotient of a Kripke structure. (Labelled transition systems are converted to Kripke structures before the main algorithm). The file accompanies the planned publication in the ACM Trans. Comput. Log. Log. special issue for TACAS 2016, to appear in 2017.

Author
David N. Jansen, Radboud Universiteit, Nijmegen, The Netherlands

Definition in file liblts_bisim_gjkw.cpp.

Macro Definition Documentation

◆ PARANOID_CHECK

#define PARANOID_CHECK

Definition at line 29 of file liblts_bisim_gjkw.cpp.