now workspaces for modular compilation (maybe faster)

rsprocess/src/environment.rs

@@ -0,0 +1,813 @@
+use std::cmp;
+use std::collections::{HashMap, HashSet};
+use std::fmt::Debug;
+use std::rc::Rc;
+
+use serde::{Deserialize, Serialize};
+
+use super::choices::{BasicChoices, Choices, PositiveChoices};
+use super::element::IdType;
+use super::process::{BasicProcess, PositiveProcess, Process};
+use super::reaction::{
+    BasicReaction, ExtensionReaction, PositiveReaction, Reaction,
+};
+use super::set::{BasicSet, PositiveSet, Set};
+use super::translator::{Formatter, PrintableWithTranslator, Translator};
+
+pub trait BasicEnvironment
+where
+    Self: Clone + Debug + Default + Serialize + PrintableWithTranslator,
+    for<'a> Self: Deserialize<'a>,
+{
+    type Id;
+    type Set: BasicSet;
+    type Choices: BasicChoices;
+    type Process: BasicProcess<Set = Self::Set, Id = Self::Id>;
+    type Reaction: BasicReaction<Set = Self::Set>;
+
+    fn get(&self, k: Self::Id) -> Option<&Self::Process>;
+    fn all_elements(&self) -> Self::Set;
+    fn unfold(
+        &self,
+        context: &Self::Process,
+        entities: &Self::Set,
+    ) -> Result<Self::Choices, String>;
+}
+
+pub trait ExtensionsEnvironment: BasicEnvironment {
+    fn iter(&self) -> <&Self as IntoIterator>::IntoIter
+    where
+        for<'b> &'b Self: IntoIterator;
+}
+
+impl<T: BasicEnvironment> ExtensionsEnvironment for T {
+    fn iter(&self) -> <&Self as IntoIterator>::IntoIter
+    where
+        for<'b> &'b Self: IntoIterator,
+    {
+        self.into_iter()
+    }
+}
+
+// -----------------------------------------------------------------------------
+//                                   Loops
+// -----------------------------------------------------------------------------
+
+pub trait LoopEnvironment: BasicEnvironment {
+    #[allow(clippy::type_complexity)]
+    fn lollipops_decomposed(
+        &self,
+        reaction_rules: &[Self::Reaction],
+        available_entities: &Self::Set,
+    ) -> Vec<(Vec<Self::Set>, Vec<Self::Set>)>;
+
+    fn lollipops_prefix_len_loop_decomposed(
+        &self,
+        reaction_rules: &[Self::Reaction],
+        available_entities: &Self::Set,
+    ) -> Vec<(usize, Vec<Self::Set>)>;
+
+    fn lollipops_only_loop_decomposed(
+        &self,
+        reaction_rules: &[Self::Reaction],
+        available_entities: &Self::Set,
+    ) -> Vec<Vec<Self::Set>>;
+
+    #[allow(clippy::type_complexity)]
+    fn lollipops_decomposed_named(
+        &self,
+        reaction_rules: &[Self::Reaction],
+        available_entities: &Self::Set,
+        symb: Self::Id,
+    ) -> Option<(Vec<Self::Set>, Vec<Self::Set>)>;
+
+    fn lollipops_prefix_len_loop_decomposed_named(
+        &self,
+        reaction_rules: &[Self::Reaction],
+        available_entities: &Self::Set,
+        symb: Self::Id,
+    ) -> Option<(usize, Vec<Self::Set>)>;
+
+    fn lollipops_only_loop_decomposed_named(
+        &self,
+        reaction_rules: &[Self::Reaction],
+        available_entities: &Self::Set,
+        symb: Self::Id,
+    ) -> Option<Vec<Self::Set>>;
+}
+
+impl<T: BasicEnvironment + ExtensionsEnvironment> LoopEnvironment for T
+where
+    for<'a> &'a T: IntoIterator<Item = (&'a T::Id, &'a T::Process)>,
+    T::Id: Eq,
+{
+    /// A special case of systems is when the context recursively provides
+    /// always the same set of entities.  The corresponding computation is
+    /// infinite.  It consists of a finite sequence of states followed by a
+    /// looping sequence.  IMPORTANT: We return all loops for all X = Q.X, by
+    /// varing X.  The set of reactions Rs and the context x are constant.  Each
+    /// state of the computation is distinguished by the current entities E.
+    /// Under these assumptions, the predicate lollipop finds the Prefixes and
+    /// the Loops sequences of entities.
+    /// see lollipop
+    fn lollipops_decomposed(
+        &self,
+        reaction_rules: &[Self::Reaction],
+        available_entities: &Self::Set,
+    ) -> Vec<(Vec<Self::Set>, Vec<Self::Set>)> {
+        // FIXME: i think we are only interested in "x", not all symbols that
+        // satisfy X = pre(Q, rec(X))
+        let filtered = self.iter().filter_map(|l| l.1.filter_delta(l.0));
+
+        let find_loop_fn = |q| {
+            T::Reaction::find_loop(
+                reaction_rules,
+                available_entities.clone(),
+                q,
+            )
+        };
+
+        filtered.map(find_loop_fn).collect::<Vec<_>>()
+    }
+
+    fn lollipops_prefix_len_loop_decomposed(
+        &self,
+        reaction_rules: &[Self::Reaction],
+        available_entities: &Self::Set,
+    ) -> Vec<(usize, Vec<Self::Set>)> {
+        let filtered = self.iter().filter_map(|l| l.1.filter_delta(l.0));
+
+        let find_loop_fn = |q| {
+            T::Reaction::find_prefix_len_loop(
+                reaction_rules,
+                available_entities.clone(),
+                q,
+            )
+        };
+
+        filtered.map(find_loop_fn).collect::<Vec<_>>()
+    }
+
+    /// see loop
+    fn lollipops_only_loop_decomposed(
+        &self,
+        reaction_rules: &[Self::Reaction],
+        available_entities: &Self::Set,
+    ) -> Vec<Vec<Self::Set>> {
+        let filtered = self.iter().filter_map(|l| l.1.filter_delta(l.0));
+
+        let find_loop_fn = |q| {
+            T::Reaction::find_only_loop(reaction_rules, available_entities, q)
+        };
+
+        filtered.map(find_loop_fn).collect::<Vec<_>>()
+    }
+
+    /// A special case of systems is when the context recursively provides
+    /// always the same set of entities.  The corresponding computation is
+    /// infinite.  It consists of a finite sequence of states followed by a
+    /// looping sequence.  IMPORTANT: We return all loops for all X = Q.X, by
+    /// varing X.  The set of reactions Rs and the context x are constant.  Each
+    /// state of the computation is distinguished by the current entities E.
+    /// Under these assumptions, the predicate lollipop finds the Prefixes and
+    /// the Loops sequences of entities.
+    /// see lollipop
+    fn lollipops_decomposed_named(
+        &self,
+        reaction_rules: &[Self::Reaction],
+        available_entities: &Self::Set,
+        symb: Self::Id,
+    ) -> Option<(Vec<Self::Set>, Vec<Self::Set>)> {
+        let filtered = self
+            .iter()
+            .filter_map(|l| {
+                if *l.0 == symb {
+                    l.1.filter_delta(&symb)
+                } else {
+                    None
+                }
+            })
+            .next();
+
+        let find_loop_fn = |q| {
+            T::Reaction::find_loop(
+                reaction_rules,
+                available_entities.clone(),
+                q,
+            )
+        };
+
+        filtered.map(find_loop_fn)
+    }
+
+    fn lollipops_prefix_len_loop_decomposed_named(
+        &self,
+        reaction_rules: &[Self::Reaction],
+        available_entities: &Self::Set,
+        symb: Self::Id,
+    ) -> Option<(usize, Vec<Self::Set>)> {
+        let filtered = self
+            .iter()
+            .filter_map(|l| {
+                if *l.0 == symb {
+                    l.1.filter_delta(&symb)
+                } else {
+                    None
+                }
+            })
+            .next();
+
+        let find_loop_fn = |q| {
+            T::Reaction::find_prefix_len_loop(
+                reaction_rules,
+                available_entities.clone(),
+                q,
+            )
+        };
+
+        filtered.map(find_loop_fn)
+    }
+
+    /// see loop
+    fn lollipops_only_loop_decomposed_named(
+        &self,
+        reaction_rules: &[Self::Reaction],
+        available_entities: &Self::Set,
+        symb: Self::Id,
+    ) -> Option<Vec<Self::Set>> {
+        let filtered = self
+            .iter()
+            .filter_map(|l| {
+                if *l.0 == symb {
+                    l.1.filter_delta(&symb)
+                } else {
+                    None
+                }
+            })
+            .next();
+
+        let find_loop_fn = |q| {
+            T::Reaction::find_only_loop(reaction_rules, available_entities, q)
+        };
+
+        filtered.map(find_loop_fn)
+    }
+}
+
+// -----------------------------------------------------------------------------
+
+#[derive(Clone, Debug, Default, Serialize, Deserialize)]
+pub struct Environment {
+    definitions: HashMap<IdType, Process>,
+}
+
+impl BasicEnvironment for Environment {
+    type Process = Process;
+    type Set = Set;
+    type Choices = Choices;
+    type Id = IdType;
+    type Reaction = Reaction;
+
+    fn get(&self, k: IdType) -> Option<&Process> {
+        self.definitions.get(&k)
+    }
+
+    fn all_elements(&self) -> Set {
+        let mut acc = Set::default();
+        for (_, process) in self.definitions.iter() {
+            acc.push(&process.all_elements());
+        }
+        acc
+    }
+
+    /// unfold returns the list of choices for the context given the process
+    /// definitions environment. choices::Choices is a list of context moves
+    /// mapping a set of entities and the continuation.
+    /// see unfold
+    fn unfold(
+        &self,
+        context_process: &Process,
+        current_entities: &Set,
+    ) -> Result<Choices, String> {
+        match context_process {
+            | Process::Nill => Ok(Choices::default()),
+            | Process::RecursiveIdentifier { identifier } => {
+                let newprocess = self.get(*identifier);
+                if let Some(newprocess) = newprocess {
+                    self.unfold(newprocess, current_entities)
+                } else {
+                    Err(format!("Missing symbol in context: {identifier}"))
+                }
+            },
+            | Process::EntitySet {
+                entities,
+                next_process,
+            } => Ok(Choices::from([(
+                Rc::new(entities.clone()),
+                Rc::clone(next_process),
+            )])),
+            | Process::Guarded {
+                reaction,
+                next_process,
+            } =>
+                if reaction.enabled(current_entities) {
+                    Ok(Choices::from([(
+                        Rc::new(reaction.products.clone()),
+                        Rc::clone(next_process),
+                    )]))
+                } else {
+                    Ok(Choices::default())
+                },
+            | Process::WaitEntity {
+                repeat,
+                repeated_process: _,
+                next_process,
+            } if *repeat <= 0 => self.unfold(next_process, current_entities),
+            | Process::WaitEntity {
+                repeat,
+                repeated_process,
+                next_process,
+            } if *repeat == 1 => {
+                let mut choices1 =
+                    self.unfold(repeated_process, current_entities)?;
+                choices1.replace(Rc::clone(next_process));
+                Ok(choices1)
+            },
+            | Process::WaitEntity {
+                repeat,
+                repeated_process,
+                next_process,
+            } => {
+                let mut choices1 =
+                    self.unfold(repeated_process, current_entities)?;
+                choices1.replace(Rc::new(Process::WaitEntity {
+                    repeat: (*repeat - 1),
+                    repeated_process: Rc::clone(repeated_process),
+                    next_process: Rc::clone(next_process),
+                }));
+                Ok(choices1)
+            },
+            | Process::Summation { children } => {
+                // short-circuits with try_fold.
+                children.iter().try_fold(Choices::default(), |mut acc, x| {
+                    match self.unfold(x, current_entities) {
+                        | Ok(mut choices) => {
+                            acc.append(&mut choices);
+                            Ok(acc)
+                        },
+                        | Err(e) => Err(e),
+                    }
+                })
+            },
+            | Process::NondeterministicChoice { children } => {
+                // short-circuits with try_fold.
+                if children.is_empty() {
+                    Ok(Choices::from(vec![(
+                        Rc::new(Set::default()),
+                        Rc::new(Process::Nill),
+                    )]))
+                } else {
+                    children.iter().try_fold(
+                        Choices::default(),
+                        |mut acc, x| {
+                            acc.shuffle(self.unfold(x, current_entities)?);
+                            Ok(acc)
+                        },
+                    )
+                }
+            },
+        }
+    }
+}
+
+impl PrintableWithTranslator for Environment {
+    fn print(
+        &self,
+        f: &mut std::fmt::Formatter,
+        translator: &Translator,
+    ) -> std::fmt::Result {
+        write!(f, "{{env:")?;
+        let mut it = self.iter().peekable();
+        while let Some(el) = it.next() {
+            if it.peek().is_none() {
+                write!(
+                    f,
+                    "({} -> {})",
+                    Formatter::from(translator, el.0),
+                    Formatter::from(translator, el.1)
+                )?;
+            } else {
+                write!(
+                    f,
+                    "({} -> {}), ",
+                    Formatter::from(translator, el.0),
+                    Formatter::from(translator, el.1)
+                )?;
+            }
+        }
+        write!(f, "}}")
+    }
+}
+
+impl IntoIterator for Environment {
+    type Item = (IdType, Process);
+    type IntoIter = std::collections::hash_map::IntoIter<IdType, Process>;
+
+    fn into_iter(self) -> Self::IntoIter {
+        self.definitions.into_iter()
+    }
+}
+
+impl<'a> IntoIterator for &'a Environment {
+    type Item = (&'a IdType, &'a Process);
+    type IntoIter = std::collections::hash_map::Iter<'a, IdType, Process>;
+
+    fn into_iter(self) -> Self::IntoIter {
+        self.definitions.iter()
+    }
+}
+
+impl<const N: usize> From<[(IdType, Process); N]> for Environment {
+    fn from(arr: [(IdType, Process); N]) -> Self {
+        Environment {
+            definitions: HashMap::from(arr),
+        }
+    }
+}
+
+impl From<&[(IdType, Process)]> for Environment {
+    fn from(arr: &[(IdType, Process)]) -> Self {
+        Environment {
+            definitions: HashMap::from_iter(arr.to_vec()),
+        }
+    }
+}
+
+impl From<Vec<(IdType, Process)>> for Environment {
+    fn from(arr: Vec<(IdType, Process)>) -> Self {
+        Environment {
+            definitions: HashMap::from_iter(arr),
+        }
+    }
+}
+
+// -----------------------------------------------------------------------------
+//                                 Confluence
+// -----------------------------------------------------------------------------
+
+impl Environment {
+    /// 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(
+        &self,
+        reaction_rules: &[Reaction],
+        entities: &[Set],
+    ) -> Option<(usize, usize, Vec<Set>)> {
+        let all_loops = self.lollipops_prefix_len_loop_decomposed(
+            reaction_rules,
+            entities.first()?,
+        );
+        let (prefix_len, hoop) = all_loops.first()?.clone();
+        let dimension = hoop.len();
+        let mut max_distance = prefix_len;
+
+        for available_entities in entities.iter().skip(1) {
+            let all_loops = self.lollipops_prefix_len_loop_decomposed(
+                reaction_rules,
+                available_entities,
+            );
+            let (prefix_len, new_hoop) = all_loops.first()?;
+
+            if new_hoop.len() != dimension || !hoop.contains(new_hoop.first()?)
+            {
+                return None;
+            }
+            max_distance = cmp::max(max_distance, *prefix_len);
+        }
+        Some((max_distance, dimension, hoop))
+    }
+
+    /// 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(
+        &self,
+        reaction_rules: &[Reaction],
+        entities: &[Set],
+        symb: IdType,
+    ) -> Option<(usize, usize, Vec<Set>)> {
+        let (prefix_len, first_hoop) = self
+            .lollipops_prefix_len_loop_decomposed_named(
+                reaction_rules,
+                entities.first()?,
+                symb,
+            )?;
+        let dimension = first_hoop.len();
+        let mut max_distance = prefix_len;
+        let hoop = first_hoop;
+
+        for available_entities in entities.iter().skip(1) {
+            let (prefix_len, new_hoop) = self
+                .lollipops_prefix_len_loop_decomposed_named(
+                    reaction_rules,
+                    available_entities,
+                    symb,
+                )?;
+
+            if new_hoop.len() != dimension || !hoop.contains(new_hoop.first()?)
+            {
+                return None;
+            }
+            max_distance = cmp::max(max_distance, prefix_len);
+        }
+        Some((max_distance, dimension, hoop))
+    }
+
+    /// 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(
+        &self,
+        reaction_rules: &[Reaction],
+        entities: &[Set],
+        symb: IdType,
+    ) -> Option<(Vec<Set>, Vec<Set>)> {
+        let (prefix, hoop) = self.lollipops_decomposed_named(
+            reaction_rules,
+            entities.first()?,
+            symb,
+        )?;
+        let mut invariant = vec![];
+        invariant.append(&mut prefix.clone());
+        invariant.append(&mut hoop.clone());
+        let dimension = hoop.len();
+
+        for available_entities in entities {
+            let (new_prefix, new_hoop) = self.lollipops_decomposed_named(
+                reaction_rules,
+                available_entities,
+                symb,
+            )?;
+            if new_hoop.len() != dimension || !hoop.contains(new_hoop.first()?)
+            {
+                return None;
+            }
+            invariant.append(&mut new_prefix.clone());
+        }
+        // remove duplicates, maybe better with sorting?
+        invariant = invariant
+            .iter()
+            .cloned()
+            .collect::<HashSet<_>>()
+            .iter()
+            .cloned()
+            .collect::<Vec<_>>();
+        Some((invariant, hoop))
+    }
+
+    /// 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: &[Self],
+        reaction_rules: &[Reaction],
+        entities: &[Set],
+        symb: IdType,
+    ) -> Option<Vec<(usize, usize, Vec<Set>)>> {
+        deltas
+            .iter()
+            .map(|q| q.confluent_named(reaction_rules, entities, symb))
+            .collect::<Option<Vec<_>>>()
+    }
+
+    /// "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: &[Self],
+        reaction_rules: &[Reaction],
+        entities: &[Set],
+        symb: IdType,
+    ) -> Option<Vec<(Vec<Set>, usize, Vec<Set>)>> {
+        deltas
+            .iter()
+            .map(|q| {
+                let (invariant, hoop) =
+                    q.invariant_named(reaction_rules, entities, symb)?;
+                let length = invariant.len();
+                Some((invariant, length, hoop))
+            })
+            .collect::<Option<Vec<_>>>()
+    }
+
+    // TODO: weak confluence
+}
+
+// -----------------------------------------------------------------------------
+
+#[derive(Clone, Debug, Default, Serialize, Deserialize)]
+pub struct PositiveEnvironment {
+    definitions: HashMap<IdType, PositiveProcess>,
+}
+
+impl BasicEnvironment for PositiveEnvironment {
+    type Id = IdType;
+    type Set = PositiveSet;
+    type Choices = PositiveChoices;
+    type Process = PositiveProcess;
+    type Reaction = PositiveReaction;
+
+    fn get(&self, k: Self::Id) -> Option<&Self::Process> {
+        self.definitions.get(&k)
+    }
+
+    fn all_elements(&self) -> Self::Set {
+        let mut acc = Self::Set::default();
+        for (_, process) in self.definitions.iter() {
+            acc.push(&process.all_elements());
+        }
+        acc
+    }
+
+    fn unfold(
+        &self,
+        context: &Self::Process,
+        entities: &Self::Set,
+    ) -> Result<Self::Choices, String> {
+        match context {
+            | PositiveProcess::Nill => Ok(Self::Choices::default()),
+            | PositiveProcess::RecursiveIdentifier { identifier } => {
+                let newprocess = self.get(*identifier);
+                if let Some(newprocess) = newprocess {
+                    self.unfold(newprocess, entities)
+                } else {
+                    Err(format!("Missing symbol in context: {identifier}"))
+                }
+            },
+            | PositiveProcess::EntitySet {
+                entities,
+                next_process,
+            } => Ok(Self::Choices::from([(
+                Rc::new(entities.clone()),
+                Rc::clone(next_process),
+            )])),
+            | PositiveProcess::Guarded {
+                reaction,
+                next_process,
+            } =>
+                if reaction.enabled(entities) {
+                    Ok(Self::Choices::from([(
+                        Rc::new(reaction.products.clone()),
+                        Rc::clone(next_process),
+                    )]))
+                } else {
+                    Ok(Self::Choices::default())
+                },
+            | PositiveProcess::WaitEntity {
+                repeat,
+                repeated_process: _,
+                next_process,
+            } if *repeat <= 0 => self.unfold(next_process, entities),
+            | PositiveProcess::WaitEntity {
+                repeat,
+                repeated_process,
+                next_process,
+            } if *repeat == 1 => {
+                let mut choices1 = self.unfold(repeated_process, entities)?;
+                choices1.replace(Rc::clone(next_process));
+                Ok(choices1)
+            },
+            | PositiveProcess::WaitEntity {
+                repeat,
+                repeated_process,
+                next_process,
+            } => {
+                let mut choices1 = self.unfold(repeated_process, entities)?;
+                choices1.replace(Rc::new(PositiveProcess::WaitEntity {
+                    repeat: (*repeat - 1),
+                    repeated_process: Rc::clone(repeated_process),
+                    next_process: Rc::clone(next_process),
+                }));
+                Ok(choices1)
+            },
+            | PositiveProcess::Summation { children } => {
+                // short-circuits with try_fold.
+                children.iter().try_fold(
+                    Self::Choices::default(),
+                    |mut acc, x| match self.unfold(x, entities) {
+                        | Ok(mut choices) => {
+                            acc.append(&mut choices);
+                            Ok(acc)
+                        },
+                        | Err(e) => Err(e),
+                    },
+                )
+            },
+            | PositiveProcess::NondeterministicChoice { children } => {
+                // short-circuits with try_fold.
+                if children.is_empty() {
+                    Ok(Self::Choices::from(vec![(
+                        Rc::new(Self::Set::default()),
+                        Rc::new(Self::Process::default()),
+                    )]))
+                } else {
+                    children.iter().try_fold(
+                        Self::Choices::default(),
+                        |mut acc, x| {
+                            acc.shuffle(self.unfold(x, entities)?);
+                            Ok(acc)
+                        },
+                    )
+                }
+            },
+        }
+    }
+}
+
+impl PrintableWithTranslator for PositiveEnvironment {
+    fn print(
+        &self,
+        f: &mut std::fmt::Formatter,
+        translator: &Translator,
+    ) -> std::fmt::Result {
+        write!(f, "{{env:")?;
+        let mut it = self.iter().peekable();
+        while let Some(el) = it.next() {
+            if it.peek().is_none() {
+                write!(
+                    f,
+                    "({} -> {})",
+                    Formatter::from(translator, el.0),
+                    Formatter::from(translator, el.1)
+                )?;
+            } else {
+                write!(
+                    f,
+                    "({} -> {}), ",
+                    Formatter::from(translator, el.0),
+                    Formatter::from(translator, el.1)
+                )?;
+            }
+        }
+        write!(f, "}}")
+    }
+}
+
+impl IntoIterator for PositiveEnvironment {
+    type Item = (IdType, PositiveProcess);
+    type IntoIter =
+        std::collections::hash_map::IntoIter<IdType, PositiveProcess>;
+
+    fn into_iter(self) -> Self::IntoIter {
+        self.definitions.into_iter()
+    }
+}
+
+impl<'a> IntoIterator for &'a PositiveEnvironment {
+    type Item = (&'a IdType, &'a PositiveProcess);
+    type IntoIter =
+        std::collections::hash_map::Iter<'a, IdType, PositiveProcess>;
+
+    fn into_iter(self) -> Self::IntoIter {
+        self.definitions.iter()
+    }
+}
+
+impl From<&Environment> for PositiveEnvironment {
+    fn from(value: &Environment) -> Self {
+        PositiveEnvironment {
+            definitions: value
+                .definitions
+                .iter()
+                .map(|(id, proc)| (*id, proc.into()))
+                .collect::<HashMap<_, _>>(),
+        }
+    }
+}
+
+impl From<Environment> for PositiveEnvironment {
+    fn from(value: Environment) -> Self {
+        (&value).into()
+    }
+}