Class BisimulationCheckerSupport<B extends Bigraph<? extends Signature<?>>,AST extends ReactionGraph<B>>
java.lang.Object
org.bigraphs.framework.simulation.equivalence.BisimulationCheckerSupport<B,AST>
- Type Parameters:
B
- the type of the state of<AST>
AST
- the type of the transition system
public class BisimulationCheckerSupport<B extends Bigraph<? extends Signature<?>>,AST extends ReactionGraph<B>>
extends Object
This implementation provides a basic extensible (template) method for computing bisimilarity of LTSs.
The type of the transition system is those whose transition relations are reaction rules, and states are bigraphs.
This class contains the checkBisimulation_Bighuggies(ReactionGraph, ReactionGraph)
method that implements the bisimulation check using a breadth-first search approach.
Depending on the complexity of the transition systems, this method needs to be adapted with more sophisticated logic.
- Author:
- Dominik Grzelak
- See Also:
-
- "https://github.com/bighuggies/bisimulation"
-
Constructor Summary
Constructors -
Method Summary
Modifier and TypeMethodDescriptionboolean
checkBisimulation_Bighuggies
(AST system1, AST system2) Bisimilarity checking using the KANELLAKIS_SMOLKA algorithm from the external "bighuggies:bisimulation" Java library.
-
Constructor Details
-
BisimulationCheckerSupport
public BisimulationCheckerSupport()
-
-
Method Details
-
checkBisimulation_Bighuggies
Bisimilarity checking using the KANELLAKIS_SMOLKA algorithm from the external "bighuggies:bisimulation" Java library.Input: Two states, one from each transition system. Output: Boolean value indicating whether the states are bisimilar.
- Parameters:
system1
-system2
-- Returns:
true
, if both systems are bisimilar; otherwisefalse
-