Saha¶
To implement the algorithm we followed the pseudocode and the analysis provided in the following paper:
Saha, Diptikalyan.
"An incremental bisimulation algorithm."
International Conference on Foundations of Software Technology
and Theoretical Computer Science.
Springer, Berlin, Heidelberg, 2007.
Using Saha’s incremental algorithm we can update the RSCP/maximum bisimulation after the addition of a new edge. While we may do the same thing computing the maximum bisimulation from scratch after the modification, Saha’s algorithm may be able to take less time on average.
Warning
Saha’s algorithm works only with integer graphs. You must convert your
graph to an isomorphic integer graph before creating the partition of
bispy.utilities.graph_entities._QBlock
.
See also
The complexity of Saha’s algorithm is highly dependent on how much the maximum bisimulation changes as a consequence of the addition of the new edge:
Therefore without an additional hypothesis on the nature of the edges added we may encounter some cases for which the incremental algorithm takes much more than re-computing the maximum bisimulation from scratch using Paige-Tarjan or Dovier-Piazza-Policriti’s algorithm.
Summary¶
Update the given RSCP/maximum bisimulation after the addition of the given new edge using Saha's incremental algorithm. |
|
Add a new edge to the graph (this is the internal BisPy representation, therefore the original graph is left untouched). |
|
Check if vblock is in the image of ublock. |
|
Check if a new strongly connected component has been created after the addition of a new edge. |
|
Check if both block1 and block2 have a non-empty intersection with the set of vertexes block_counterimage. |
|
Check if there is a causal splitter for blocks block1 and block2. |
|
Check all the condition which may prevent the union of two blocks, returns True if the blocks can be joined. |
|
Merge block1, block2 (put the vertexes of block2 into block1), deteach block2 from the partition, and check recursively if we can also merge some couples of predecessors of block1 and block2 (namely couple of blocks \(C,D\) such that |
|
We check if there is a block \(U1\) such that before the addition of the new edge \(\langle u,v \rangle\) there was a causal splitter for the couple \(([u],U1)\), and for which |
|
Preprocess the given partition to split blocks which contain leafs and non-leafs. |
|
The function MergeAndSplitPhase from the paper. |
|
Compute the updated rank of the given SCC, and propagate the change to its counterimage in the order given by the finishing time of a visit on the graph of strongly connected components of \(G\). |
|
Recursively visit the well-founded counterimage of the given vertex and update the rank. |
|
Build a list of all the vertexes in the graph sorted in increasing order of rank. |
|
Remove deteached blocks (blocks such that the attribute deteached is True) from the given list. |
Code documentation¶
- saha(old_rscp, vertexes, new_edge)¶
Update the given RSCP/maximum bisimulation after the addition of the given new edge using Saha’s incremental algorithm.
The edge must not be already in the BisPy representation of the graph (namely in the image/counterimage of the instances of
bispy.utilities.graph_entities._Vertex
in blocks of old_rscp).- Parameters
- New_edge
The new edge to be added to the graph (as a tuple of two
bispy.utilities.graph_entities._Vertex
instances, or two ints which represent the indexes of the nodes which characterize the edge). The first item represents the source of the edge, the second represents the destination.- Return type
List
[_QBlock
]- Returns
The updated RSCP/maximum bisimulation. Also rank is updated for each vertex.
- add_edge(source, destination)¶
Add a new edge to the graph (this is the internal BisPy representation, therefore the original graph is left untouched).
This function also sets the count attribute for the new edge, creating a new instance of
bispy.utilities.graph_entities._Count
if the source of the edge was a sink previously, and getting the instance from the first edge in the image otherwise.
- is_in_image(ublock, vblock)¶
Check if vblock is in the image of ublock. This is used before adding a new edge, because if the destination vertex is already in the image of the source vertex we do not need to change the partition to reach the maximum bisimulation.
Warning
ublock and vblock must be members of a stable partition, otherwise this function returns a wrong output.
- check_new_scc(current_source, destination, finishing_time_list=None, visited_vertexes=None, root_call=True)¶
Check if a new strongly connected component has been created after the addition of a new edge. This is meant to be a recursive method, therefore the new edge is not always \(\langle\) current_source, destination \(\rangle\).
This method visits \(G^{-1}\) recursively (with a DFS strategy) starting from current_source until it finds the destination vertex, in which case a new SCC is recognized.
Meanwhile it also sets the flag visited for each visited vertex to prevent visiting the same node twice. At the end of the execution the root call cleans the flag visited for each vertex by exploring each vertex in the list visited_vertexes, which is passed automatically from the root call to all its children.
It also sets the flag visited for each visited
bispy.utilities.graph_entities._QBlock
. This information is used in other parts of the algorithm.- Parameters
current_source (
_Vertex
) – The current starting point for the DFS of \(G^{-1}\).destination (
_Vertex
) – The destination vertex of the new edge.finishing_time_list (
Optional
[List
[_Vertex
]]) – An empty list which will be filled with the vertexes ordered by finishing time (first are those for which the exploaration of the image ended earlier). This feature is disabled if this argument is None.visited_vertexes (
Optional
[List
[_Vertex
]]) – An empty list which will be filled with the vertexes visited during the execution. You do not need to pass a non-None value since the root call takes care of the necessary cleanup which occurs after the execution of the function.root_call – True if this instance of the function is the root call. Passing any value other than True (from a user perspective) is going to end with an exception.
- Return type
bool
- Returns
True if a new strongly connected component has been created, False otherwise.
- both_blocks_go_or_dont_go_to_block(block1, block2, block_counterimage)¶
Check if both block1 and block2 have a non-empty intersection with the set of vertexes block_counterimage.
Usually the parameter block_counterimage contains the counterimage of a block, therefore this method may be stated like “find if both block1 and block2 go to the third block, or if both blocks do not go to that block”.
- exists_causal_splitter(block1, block2, check_visited)¶
Check if there is a causal splitter for blocks block1 and block2. A causal splitter is a block \(C\) such that
\[\textit{block1} \cap E^{-1}(C) \neq \emptyset \land \textit{block2} \cap E^{-1}(C) = \emptyset\]or viceversa.
The existence of a causal splitter prevents two blocks from being joined.
- Parameters
- Return type
bool
- Returns
True if there is a causal splitter for the two blocks, False otherwise.
- merge_condition(block1, block2, check_visited=False)¶
Check all the condition which may prevent the union of two blocks, returns True if the blocks can be joined. Some conditions are redundant, we check first those which are almost instantaneous to verify since this method is going to be called frequently.
The conditions:
Same labeling set/initial partition;
The two blocks are not the same block;
Same rank;
- One of the blocks was deteached from the partition previously (therefore
it is most likely empty at this points);
There is not a causal splitter for the two blocks.
- Parameters
block1 (
_QBlock
) – A block.block2 (
_QBlock
) – A block.check_visited (
bool
) – See the documentation ofexists_causal_splitter()
.
- Return type
bool
- recursive_merge(block1, block2)¶
Merge block1, block2 (put the vertexes of block2 into block1), deteach block2 from the partition, and check recursively if we can also merge some couples of predecessors of block1 and block2 (namely couple of blocks \(C,D\) such that
\[C \implies \textit{block1} \land D \implies \textit{block2}\]where the relation “\(\implies\)” means that there is at least one vertex of the rightmost block which is a child of the leftmost block).
If such at couple exists, the method recursively merges those two blocks, for each couple for which
merge_condition()
is True.
- merge_phase(ublock, vblock)¶
We check if there is a block \(U1\) such that before the addition of the new edge \(\langle u,v \rangle\) there was a causal splitter for the couple \(([u],U1)\), and for which
merge_condition()
now returns True on that couple.In that case we merge the two blocks using
recursive_merge()
.
- preprocess_initial_partition(qblocks)¶
Preprocess the given partition to split blocks which contain leafs and non-leafs.
- Parameters
qblocks (
List
[_QBlock
]) – A partition.
- merge_split_phase(qpartition, finishing_time_list)¶
The function MergeAndSplitPhase from the paper.
- propagate_nwf(scc, scc_finishing_time)¶
Compute the updated rank of the given SCC, and propagate the change to its counterimage in the order given by the finishing time of a visit on the graph of strongly connected components of \(G\).
- propagate_wf(vertex, well_founded_topological, scc_finishing_time)¶
Recursively visit the well-founded counterimage of the given vertex and update the rank. The visit is in increasing order of rank (this is needed in order to obtain the correct result).
- Parameters
vertex (
_Vertex
) – The vertex to whose counterimage we intend to propagate the change of the rank. The rank of this argument must already be updated, since it is left untouched after the execution.well_founded_topological (
List
[_Vertex
]) – List of well founded vertexes of the whole graph in topological order.
- build_well_founded_topological_list(partition, source, max_rank)¶
Build a list of all the vertexes in the graph sorted in increasing order of rank.
We ignore all the nodes which do not have rank = \(-\infty\) and have rank lower that the rank of the source vertex of the new edge.
- Parameters
partition (
List
[_QBlock
]) – A partition of the graph from which we obtain the instances ofbispy.utilities.graph_entities._Vertex
. All the nodes in the same block must have the same rank.source (
_Vertex
) – The source vertex of the new edge.max_rank (
int
) – The maximum rank of a vertex in this graph, used to create a list of the appropriate size.
- Return type
List
[_Vertex
]