Skip to content

Commit

Permalink
Module restructuring in scan_core
Browse files Browse the repository at this point in the history
Signed-off-by: Enrico Ghiorzi <[email protected]>
  • Loading branch information
EnricoGhiorzi committed May 21, 2024
1 parent f64600d commit 5c4ad68
Show file tree
Hide file tree
Showing 6 changed files with 55 additions and 25 deletions.
20 changes: 14 additions & 6 deletions scan_core/src/channel_system.rs
Original file line number Diff line number Diff line change
@@ -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);
Expand Down
7 changes: 7 additions & 0 deletions scan_core/src/grammar.rs
Original file line number Diff line number Diff line change
@@ -1,3 +1,10 @@
//! The language used by PGs and CSs.
//!
//! The type [`Expression<V>`] 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,
Expand Down
9 changes: 5 additions & 4 deletions scan_core/src/lib.rs
Original file line number Diff line number Diff line change
@@ -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::*;
14 changes: 10 additions & 4 deletions scan_core/src/program_graph.rs
Original file line number Diff line number Diff line change
@@ -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.
Expand All @@ -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<Var>;
pub type PgExpression = Expression<Var>;

#[derive(Debug, Clone, Error)]
pub enum PgError {
Expand Down
5 changes: 1 addition & 4 deletions scan_fmt_xml/src/cs_builder.rs
Original file line number Diff line number Diff line change
@@ -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)]
Expand Down Expand Up @@ -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"))
Expand Down
25 changes: 18 additions & 7 deletions scan_fmt_xml/src/parser.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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 {
Expand Down Expand Up @@ -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")]
Expand Down Expand Up @@ -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<R: BufRead>(
Expand Down

0 comments on commit 5c4ad68

Please sign in to comment.