Converting to library and commenting code

refactoring and removing useless functions

src/rsprocess/confluence.rs

@@ -1,5 +1,3 @@
-#![allow(dead_code)]
-
 use super::perpetual::{
     lollipops_decomposed_named, lollipops_prefix_len_loop_decomposed,
     lollipops_prefix_len_loop_decomposed_named,
@@ -9,7 +7,13 @@ use super::translator::IdType;
 use std::cmp;
 use std::collections::HashSet;
 
-// see confluent, confluents
+
+/// Two set of entities E1 and E2 are confluent w.r.t. the perpetual context
+/// delta iff they reach the same loop.
+/// confluent checks if all the sets of entities in ```entities``` are confluent
+/// and if so returns the maximal length of prefixes traversed to reached the
+/// loop, its dimension (length) and the loop.
+/// see confluent, confluents
 pub fn confluent(
     delta: &RSenvironment,
     reaction_rules: &[RSreaction],
@@ -27,7 +31,6 @@ pub fn confluent(
             lollipops_prefix_len_loop_decomposed(delta,
 						 reaction_rules,
 						 available_entities);
-        // FIXME we take just the first? do we compare all?
         let (prefix_len, new_hoop) = all_loops.first()?;
 
         if new_hoop.len() != dimension || !hoop.contains(new_hoop.first()?) {
@@ -38,7 +41,12 @@ pub fn confluent(
     Some((max_distance, dimension, hoop))
 }
 
-// see confluent, confluents
+/// Two set of entities E1 and E2 are confluent w.r.t. the perpetual context Q
+/// iff they reach the same loop.
+/// The predicate confluent(Rs,Q,Es,Loop,Distance,Dimension) checks if all the
+/// sets of entities in Es are confluent and if so returns the Loop, the maximal
+/// length of prefixes traversed to reached the loop and its dimension (length).
+/// see confluent, confluents
 pub fn confluent_named(
     delta: &RSenvironment,
     reaction_rules: &[RSreaction],
@@ -72,7 +80,9 @@ pub fn confluent_named(
 
 // -----------------------------------------------------------------------------
 
-// see invariant
+/// invariant_named checks if all the sets of entities in ```entities``` are
+/// confluent and if so returns the set of all traversed states, together with the loop.
+/// see invariant
 pub fn invariant_named(
     delta: &RSenvironment,
     reaction_rules: &[RSreaction],
@@ -113,7 +123,18 @@ pub fn invariant_named(
 
 // -----------------------------------------------------------------------------
 
-// see loop_confluent
+/// Suppose the context has the form
+/// Q1. ... Q1.Q2. ... Q2. ... Qn. ... Qn. ...
+/// and that each context Q1, Q2, ... , Q(n-1) is provided for a large number
+/// of times, enough to stabilize the system in a loop (while Qn is provided
+/// infinitely many times).  Then it can be the case that when the context
+/// switches from Qi to Q(i+1), no matter what is the current state of the loop
+/// for Qi at the moment of the switching, the system will stabilize in the same
+/// loop for Q(i+1): if this is the case the system is called "loop confluent".
+/// loop_confluent_named checks this property over the list of contexts
+/// [Q1,Q2,...,Qn] and returns the lists of Loops, Distances and Dimensions for
+/// all Qi's.
+/// see loop_confluent
 pub fn loop_confluent_named(
     deltas: &[RSenvironment],
     reaction_rules: &[RSreaction],
@@ -126,7 +147,12 @@ pub fn loop_confluent_named(
         .collect::<Option<Vec<_>>>()
 }
 
-// see strong_confluent
+/// "strong confluence" requires loop confluence and additionally check
+/// that even if the context is switched BEFORE REACHING THE LOOP for Qi
+/// the traversed states are still confluent for Q(i+1)
+/// IMPORTANT: this notion of confluence assumes each context can be executed 0
+/// or more times
+/// see strong_confluent
 #[allow(clippy::type_complexity)]
 pub fn strong_confluent_named(
     deltas: &[RSenvironment],
@@ -146,3 +172,5 @@ pub fn strong_confluent_named(
         })
         .collect::<Option<Vec<_>>>()
 }
+
+// TODO: weak confluence