Refactoring JANI frontend

Cargo.toml

@@ -1,6 +1,6 @@
 [package]
 name = "smc_scan"
-version = "0.2.1"
+version = "0.3.0"
 edition = "2024"
 description = "Statistical model checker for large concurrent systems."
 documentation = "https://convince-project.github.io/scan/crates/scan/index.html"
@@ -9,33 +9,41 @@ repository = "https://github.com/convince-project/scan"
 readme = "README.md"
 license = "Apache-2.0"
 keywords = ["verification", "model-checking"]
-categories = ["compilers", "concurrency", "parser-implementations", "science::robotics", "simulation"]
-exclude = [
-    "scan_book/*",
-    ".github/*"
+categories = [
+  "compilers",
+  "concurrency",
+  "parser-implementations",
+  "science::robotics",
+  "simulation"
 ]
+exclude = ["scan_book/*", ".github/*"]
 
 [lib]
-name = "scan"     # The name of the target.
-crate-type = ["lib"]   # The crate types to generate.
+name = "scan"  # The name of the target.
+crate-type = ["lib"]  # The crate types to generate.
 
 [[bin]]
-name = "scan"     # The name of the target.
+name = "scan"  # The name of the target.
 path = "src/main.rs"
 
 [profile.release]
 lto = true
 codegen-units = 1
-# debug = true # only to run profiling
 
 # See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html
 [workspace]
-members = ["scan_core", "scan_scxml", "scan_jani", "scan_promela"]
+members = [
+  "scan_core",
+  "scan_scxml",
+  "scan_jani",
+  "scan_promela",
+  "scan_pmtl",
+  "scan_mtl"
+]
 
 [workspace.dependencies]
 anyhow = "1.0.102"
 csv = "1.4.0"
-flate2 = { version = "1.1.9", features = ["zlib-rs"], default-features = false }
 log = "0.4.29"
 serde = { version = "1.0.228", features = ["derive"] }
 serde_json = "1.0.149"
@@ -49,9 +57,9 @@ env_logger = "0.11.10"
 human-panic = "2.0.8"
 indicatif = { version = "0.18.4", features = ["improved_unicode"] }
 log = { workspace = true }
-smc_scan_core = { version = "0.1.1", path = "scan_core" }
-smc_scan_jani = { version = "0.1.1", path = "scan_jani" }
-smc_scan_scxml = { version = "0.2.0", path = "scan_scxml" }
-smc_scan_promela = { version = "0.1.1", path = "scan_promela" }
+smc_scan_core = { version = "0.2.0", path = "scan_core" }
+smc_scan_jani = { version = "0.2.0", path = "scan_jani" }
+smc_scan_scxml = { version = "0.3.0", path = "scan_scxml" }
+smc_scan_promela = { version = "0.2.0", path = "scan_promela" }
 serde = { workspace = true }
 serde_json = { workspace = true }

scan_core/Cargo.toml

@@ -1,6 +1,6 @@
 [package]
 name = "smc_scan_core"
-version = "0.1.1"
+version = "0.2.0"
 edition = "2024"
 description = "Core module for the Scan model checker."
 documentation = "https://convince-project.github.io/scan/crates/scan_core/index.html"
@@ -9,15 +9,22 @@ repository = "https://github.com/convince-project/scan"
 license = "Apache-2.0"
 readme = "README.md"
 keywords = ["verification", "model-checking"]
-categories = ["compilers", "concurrency", "parser-implementations", "science::robotics", "simulation"]
+categories = [
+  "compilers",
+  "concurrency",
+  "parser-implementations",
+  "science::robotics",
+  "simulation"
+]
 
 [lib]
-name = "scan_core"     # The name of the target.
-crate-type = ["lib"]   # The crate types to generate.
+name = "scan_core"  # The name of the target.
+crate-type = ["lib"]  # The crate types to generate.
 
 [dependencies]
 thiserror = { workspace = true }
 log = { workspace = true }
+flate2 = { version = "1.1.9", features = ["zlib-rs"], default-features = false }
 rand = { version = "0.10.1" }
 rayon = "1.12.0"
 smallvec = "1.15.1"

scan_core/src/channel_system.rs

@@ -278,6 +278,15 @@ pub enum EventType {
     ProbeFullQueue,
 }
 
+/// The capacity type of a channel:
+#[derive(Debug, Clone, Copy)]
+pub enum ChannelCapacity {
+    /// A (in)finite-capacity FIFO queue.
+    Queue(Option<usize>),
+    /// A channel that receives messages but never returns them.
+    Sink,
+}
+
 /// A definition object for a CS.
 /// It represents the abstract definition of a CS.
 ///
@@ -314,7 +323,7 @@ pub enum EventType {
 /// ```
 #[derive(Debug, Clone)]
 pub struct ChannelSystem {
-    channels: Vec<(Vec<Type>, Option<usize>)>,
+    channels: Vec<(Vec<Type>, ChannelCapacity)>,
     communications: Vec<Option<(Channel, Message)>>,
     communications_pg_idxs: Vec<usize>,
     program_graphs: Vec<ProgramGraph>,
@@ -328,18 +337,24 @@ impl ChannelSystem {
     ///
     /// See also [`ProgramGraph::new_instance`].
     pub fn new_instance<'def>(&'def self) -> ChannelSystemRun<'def> {
+        let pgs = self.program_graphs.len() as u16;
+        let mut pg_list = Vec::from_iter((0..pgs).map(PgId));
+        pg_list.shrink_to_fit();
+
         ChannelSystemRun {
             rng: rand::make_rng(),
             time: 0,
             program_graphs: Vec::from_iter(
                 self.program_graphs.iter().map(|pgdef| pgdef.new_instance()),
             ),
-            message_queue: Vec::from_iter(self.channels.iter().map(|(types, cap)| {
-                cap.map_or_else(VecDeque::new, |cap| {
+            message_queue: Vec::from_iter(self.channels.iter().map(|(types, cap)| match cap {
+                ChannelCapacity::Queue(queue) => queue.map_or_else(VecDeque::new, |cap| {
                     VecDeque::with_capacity(types.len() * cap)
-                })
+                }),
+                ChannelCapacity::Sink => VecDeque::new(),
             })),
             def: self,
+            pg_list,
         }
     }
 
@@ -356,7 +371,7 @@ impl ChannelSystem {
     /// Returns the list of defined channels, given as the pair of their type and capacity
     /// (where `None` denotes channels with infinite capacity, and `Some` denotes channels with finite capacity).
     #[inline]
-    pub fn channels(&self) -> &Vec<(Vec<Type>, Option<usize>)> {
+    pub fn channels(&self) -> &Vec<(Vec<Type>, ChannelCapacity)> {
         &self.channels
     }
 }
@@ -374,6 +389,7 @@ pub struct ChannelSystemRun<'def> {
     message_queue: Vec<VecDeque<Val>>,
     program_graphs: Vec<ProgramGraphRun<'def>>,
     def: &'def ChannelSystem,
+    pg_list: Vec<PgId>,
 }
 
 impl<'def> ChannelSystemRun<'def> {
@@ -414,15 +430,23 @@ impl<'def> ChannelSystemRun<'def> {
             })
     }
 
-    pub(crate) fn montecarlo_execution(&mut self) -> Option<Event> {
-        let pgs = self.program_graphs.len();
-        let mut pg_vec = Vec::from_iter((0..pgs as u16).map(PgId));
+    pub(crate) fn montecarlo_execution(&mut self) -> Option<(Action, Event)> {
         let mut rand1 = SmallRng::from_rng(&mut self.rng);
         let mut rand2 = SmallRng::from_rng(&mut self.rng);
-        while !pg_vec.is_empty() {
-            let pg_id = pg_vec.swap_remove(self.rng.random_range(0..pg_vec.len()));
+        // Setting pgs_left as length resets the queue
+        let mut pgs_left = self.pg_list.len();
+        while pgs_left > 0 {
+            // Select random pg within 0..pgs_left
+            let pg_select = self.rng.random_range(0..pgs_left);
+            let pg_id = self.pg_list[pg_select];
+            // Swap selected pg with last element of the queue (possibly itself, probably not worth checking)
+            // Decrease the length of the queue (so that selected element is removed)
+            pgs_left -= 1;
+            self.pg_list.swap(pg_select, pgs_left);
             // Execute randomly chosen transitions on the picked PG until an event is generated,
             // or no more transition is possible
+            // NOTE: Special treatment for PGs with single-location state for optimization of this common case.
+            // Hopefully it will be possible to treat all cases in a general way eventually.
             if self.program_graphs[pg_id.0 as usize].current_states().len() == 1 {
                 while let Some((action, post_state)) = self.program_graphs[pg_id.0 as usize]
                     .nosync_possible_transitions()
@@ -442,7 +466,7 @@ impl<'def> ChannelSystemRun<'def> {
                         .transition(pg_id, Action(pg_id, action), &[post_state])
                         .expect("successful transition");
                     if event.is_some() {
-                        return event;
+                        return event.map(|ev| (Action(pg_id, action), ev));
                     }
                 }
             } else {
@@ -465,7 +489,7 @@ impl<'def> ChannelSystemRun<'def> {
                         .transition(pg_id, Action(pg_id, action), post_states.as_slice())
                         .expect("successful transition");
                     if event.is_some() {
-                        return event;
+                        return event.map(|ev| (Action(pg_id, action), ev));
                     }
                 }
             }
@@ -479,14 +503,20 @@ impl<'def> ChannelSystemRun<'def> {
         let (_, capacity) = self.def.channels[channel_idx];
         let len = self.message_queue[channel_idx].len();
         // Channel capacity must never be exceeded!
-        debug_assert!(capacity.is_none_or(|cap| len <= cap));
+        // debug_assert!(capacity.is_none_or(|cap| len <= cap));
         // NOTE FIXME currently handshake is unsupported
         // !matches!(capacity, Some(0))
-        match message {
-            Message::Send => capacity.is_none_or(|cap| len < cap),
-            Message::Receive => len > 0,
-            Message::ProbeFullQueue => capacity.is_some_and(|cap| len == cap),
-            Message::ProbeEmptyQueue => len == 0,
+        match capacity {
+            ChannelCapacity::Queue(capacity) => match message {
+                Message::Send => capacity.is_none_or(|cap| len < cap),
+                Message::Receive => len > 0,
+                Message::ProbeFullQueue => capacity.is_some_and(|cap| len == cap),
+                Message::ProbeEmptyQueue => len == 0,
+            },
+            ChannelCapacity::Sink => match message {
+                Message::Send | Message::ProbeEmptyQueue => true,
+                Message::Receive | Message::ProbeFullQueue => false,
+            },
         }
     }
 
@@ -499,25 +529,32 @@ impl<'def> ChannelSystemRun<'def> {
             let (_, capacity) = self.def.channels[channel.0 as usize];
             let len = self.message_queue[channel.0 as usize].len();
             // Channel capacity must never be exceeded!
-            assert!(capacity.is_none_or(|cap| len <= cap));
-            match message {
-                Message::Send if capacity.is_some_and(|cap| len >= cap) => {
-                    Err(CsError::OutOfCapacity(channel))
-                }
-                Message::Receive if len == 0 => Err(CsError::Empty(channel)),
-                Message::ProbeEmptyQueue | Message::ProbeFullQueue
-                    if matches!(capacity, Some(0)) =>
-                {
-                    Err(CsError::ProbingHandshakeChannel(channel))
-                }
-                Message::ProbeFullQueue if capacity.is_none() => {
-                    Err(CsError::ProbingInfiniteQueue(channel))
-                }
-                Message::ProbeEmptyQueue if len > 0 => Err(CsError::NotEmpty(channel)),
-                Message::ProbeFullQueue if capacity.is_some_and(|cap| len < cap) => {
-                    Err(CsError::NotFull(channel))
-                }
-                _ => Ok(()),
+            // assert!(capacity.is_none_or(|cap| len <= cap));
+            match capacity {
+                ChannelCapacity::Queue(capacity) => match message {
+                    Message::Send if capacity.is_some_and(|cap| len >= cap) => {
+                        Err(CsError::OutOfCapacity(channel))
+                    }
+                    Message::Receive if len == 0 => Err(CsError::Empty(channel)),
+                    Message::ProbeEmptyQueue | Message::ProbeFullQueue
+                        if matches!(capacity, Some(0)) =>
+                    {
+                        Err(CsError::ProbingHandshakeChannel(channel))
+                    }
+                    Message::ProbeFullQueue if capacity.is_none() => {
+                        Err(CsError::ProbingInfiniteQueue(channel))
+                    }
+                    Message::ProbeEmptyQueue if len > 0 => Err(CsError::NotEmpty(channel)),
+                    Message::ProbeFullQueue if capacity.is_some_and(|cap| len < cap) => {
+                        Err(CsError::NotFull(channel))
+                    }
+                    _ => Ok(()),
+                },
+                ChannelCapacity::Sink => match message {
+                    Message::Send | Message::ProbeEmptyQueue => Ok(()),
+                    Message::ProbeFullQueue => Err(CsError::NotFull(channel)),
+                    Message::Receive => Err(CsError::Empty(channel)),
+                },
             }
         } else {
             Ok(())
@@ -548,8 +585,10 @@ impl<'def> ChannelSystemRun<'def> {
             let (_, capacity) = self.def.channels[channel.0 as usize];
             let event_type = match message {
                 Message::Send
-                    if capacity
-                        .is_some_and(|cap| self.message_queue[channel.0 as usize].len() >= cap) =>
+                    if let ChannelCapacity::Queue(capacity) = capacity
+                        && capacity.is_some_and(|cap| {
+                            self.message_queue[channel.0 as usize].len() >= cap
+                        }) =>
                 {
                     return Err(CsError::OutOfCapacity(channel));
                 }
@@ -564,7 +603,9 @@ impl<'def> ChannelSystemRun<'def> {
                             &mut self.rng,
                         )
                         .map_err(|err| CsError::ProgramGraph(pg_id, err))?;
-                    self.message_queue[channel.0 as usize].extend(vals.iter().copied());
+                    if matches!(capacity, ChannelCapacity::Queue(_)) {
+                        self.message_queue[channel.0 as usize].extend(vals.iter().copied());
+                    }
                     EventType::Send(vals)
                 }
                 Message::Receive if self.message_queue[channel.0 as usize].is_empty() => {
@@ -588,7 +629,7 @@ impl<'def> ChannelSystemRun<'def> {
                     EventType::Receive(vals)
                 }
                 Message::ProbeEmptyQueue | Message::ProbeFullQueue
-                    if matches!(capacity, Some(0)) =>
+                    if matches!(capacity, ChannelCapacity::Queue(Some(0))) =>
                 {
                     return Err(CsError::ProbingHandshakeChannel(channel));
                 }
@@ -608,28 +649,29 @@ impl<'def> ChannelSystemRun<'def> {
                         .map_err(|err| CsError::ProgramGraph(pg_id, err))?;
                     EventType::ProbeEmptyQueue
                 }
-                Message::ProbeFullQueue
-                    if capacity
-                        .is_some_and(|cap| self.message_queue[channel.0 as usize].len() < cap) =>
-                {
-                    return Err(CsError::NotFull(channel));
-                }
-                Message::ProbeFullQueue if capacity.is_none() => {
-                    return Err(CsError::ProbingInfiniteQueue(channel));
-                }
-                Message::ProbeFullQueue => {
-                    let _ = self.program_graphs[pg_id.0 as usize]
-                        .send(
-                            action.1,
-                            post.iter()
-                                .map(|loc| loc.1)
-                                .collect::<SmallVec<[PgLocation; 8]>>()
-                                .as_slice(),
-                            &mut self.rng,
-                        )
-                        .map_err(|err| CsError::ProgramGraph(pg_id, err))?;
-                    EventType::ProbeFullQueue
-                }
+                Message::ProbeFullQueue => match capacity {
+                    ChannelCapacity::Queue(None) => {
+                        return Err(CsError::ProbingInfiniteQueue(channel));
+                    }
+                    ChannelCapacity::Queue(Some(capacity)) => {
+                        if self.message_queue[channel.0 as usize].len() >= capacity {
+                            let _ = self.program_graphs[pg_id.0 as usize]
+                                .send(
+                                    action.1,
+                                    post.iter()
+                                        .map(|loc| loc.1)
+                                        .collect::<SmallVec<[PgLocation; 8]>>()
+                                        .as_slice(),
+                                    &mut self.rng,
+                                )
+                                .map_err(|err| CsError::ProgramGraph(pg_id, err))?;
+                            EventType::ProbeFullQueue
+                        } else {
+                            return Err(CsError::NotFull(channel));
+                        }
+                    }
+                    ChannelCapacity::Sink => return Err(CsError::NotFull(channel)),
+                },
             };
             Ok(Some(Event {
                 pg_id,