diff --git a/scan_core/src/channel_system.rs b/scan_core/src/channel_system.rs index 4cff9cf..de2e323 100644 --- a/scan_core/src/channel_system.rs +++ b/scan_core/src/channel_system.rs @@ -1,11 +1,19 @@ -use super::grammar::*; - +//! Implementation of the CS model of computation. +//! +//! Channel systems comprises multiple program graphs executing asynchronously +//! and sending and retreiving messages from channels. +//! +//! Analogously to PGs, a CS is defined through a [`ChannelSystemBuilder`], +//! by adding new PGs and channels. +//! Each PG in the CS can be given new locations, actions, effects, guards and transitions. +//! Then, a [`ChannelSystem`] is built from the [`ChannelSystemBuilder`] +//! and can be executed by performing transitions, +//! though the definition of the CS itself can no longer be altered. + +use crate::grammar::*; +use crate::program_graph::*; use std::{collections::HashMap, error::Error, fmt, rc::Rc}; -use crate::{ - Action, Location, PgError, PgExpression, ProgramGraph, ProgramGraphBuilder, Type, Val, Var, -}; - // Use of "Newtype" pattern to define different types of indexes. #[derive(Debug, Clone, Copy, Hash, PartialEq, Eq)] pub struct PgId(usize); diff --git a/scan_core/src/grammar.rs b/scan_core/src/grammar.rs index ee733ad..b9b2fa7 100644 --- a/scan_core/src/grammar.rs +++ b/scan_core/src/grammar.rs @@ -1,3 +1,10 @@ +//! The language used by PGs and CSs. +//! +//! The type [`Expression`] encodes the used language, +//! where `V` is the type parameter of variables. +//! The language features base types and product types, +//! Boolean logic and basic arithmetic expressions. + #[derive(Debug, Clone, Hash, PartialEq, Eq)] pub enum Type { Unit, diff --git a/scan_core/src/lib.rs b/scan_core/src/lib.rs index abcdb80..3784a68 100644 --- a/scan_core/src/lib.rs +++ b/scan_core/src/lib.rs @@ -1,7 +1,8 @@ -mod channel_system; +//! Implementation of *program graphs* (PG) and *channel systems* (CS) formalisms +//! for use in the SCAN model checker. + +pub mod channel_system; mod grammar; -mod program_graph; +pub mod program_graph; -pub use channel_system::*; pub use grammar::*; -pub use program_graph::*; diff --git a/scan_core/src/program_graph.rs b/scan_core/src/program_graph.rs index 8ffd5b3..d309df6 100644 --- a/scan_core/src/program_graph.rs +++ b/scan_core/src/program_graph.rs @@ -1,8 +1,14 @@ -use super::grammar::*; +//! Implementation of the PG model of computation. +//! +//! A PG is defined through a [`ProgramGraphBuilder`], +//! by adding new locations, actions, effects, guards and transitions. +//! Then, a [`ProgramGraph`] is built from the [`ProgramGraphBuilder`] +//! and can be executed by performing transitions, +//! though the definition of the PG itself can no longer be altered. -// TODO: use fast hasher +// TODO: use fast hasher (?) +use super::grammar::*; use std::{collections::HashMap, rc::Rc}; - use thiserror::Error; // Use of "Newtype" pattern to define different types of indexes. @@ -17,7 +23,7 @@ pub struct Action(usize); #[derive(Debug, Clone, Copy, Hash, PartialEq, Eq)] pub struct Var(usize); -pub type PgExpression = super::grammar::Expression; +pub type PgExpression = Expression; #[derive(Debug, Clone, Error)] pub enum PgError { diff --git a/scan_fmt_xml/src/cs_builder.rs b/scan_fmt_xml/src/cs_builder.rs index 437b913..4f0f06d 100644 --- a/scan_fmt_xml/src/cs_builder.rs +++ b/scan_fmt_xml/src/cs_builder.rs @@ -1,7 +1,7 @@ use crate::parser::*; use anyhow::anyhow; use log::{info, trace}; -use scan_core::*; +use scan_core::{channel_system::*, *}; use std::collections::{HashMap, HashSet}; #[derive(Debug)] @@ -1141,9 +1141,6 @@ impl Sc2CsVisitor { .ok_or(anyhow!("not utf8"))?; match ident { "_event" => todo!(), - // enum_const if self.enums.contains_key(&(enum_type, enum_const.to_owned())) => { - // todo!() - // } var_ident => vars .get(var_ident) .ok_or(anyhow!("unknown variable")) diff --git a/scan_fmt_xml/src/parser.rs b/scan_fmt_xml/src/parser.rs index c5f7b83..e9a9b20 100644 --- a/scan_fmt_xml/src/parser.rs +++ b/scan_fmt_xml/src/parser.rs @@ -20,7 +20,7 @@ pub use self::bt::*; pub use self::fsm::*; pub use self::omg_types::*; pub use self::vocabulary::*; -use scan_core::{ChannelSystem, ChannelSystemBuilder, CsError}; +use scan_core::channel_system::*; #[derive(Error, Debug)] pub enum ParserErrorType { @@ -56,8 +56,6 @@ pub enum ParserErrorType { AlreadyDeclared(String), #[error("unknown model of computation: `{0}`")] UnknownMoC(String), - #[error("unknown type of skill: `{0}`")] - UnknownSkillType(String), #[error("not in a state")] NotAState, #[error("behavior tree missing root node")] @@ -288,13 +286,26 @@ impl Parser { MoC::Bt(bt) } moc => { - return Err(anyhow!("unknown MoC {moc}")); + return Err(anyhow::Error::new(ParserError( + reader.buffer_position(), + ParserErrorType::UnknownMoC(moc.to_string()), + ))); } }; let process = Process { moc }; - // Here it should be checked that no process was already in the list under the same name - self.process_list.insert(process_id, process); - Ok(()) + // Add process to list and check that no process was already in the list under the same name + if self + .process_list + .insert(process_id.to_owned(), process) + .is_none() + { + Ok(()) + } else { + Err(anyhow::Error::new(ParserError( + reader.buffer_position(), + ParserErrorType::AlreadyDeclared(process_id), + ))) + } } fn parse_types(