fmt
This commit is contained in:
@ -1,8 +1,9 @@
|
||||
use execution::presets;
|
||||
use lalrpop_util::ParseError;
|
||||
use std::fmt::Display;
|
||||
use grammar::grammar;
|
||||
|
||||
use ::grammar::user_error::{UserError, UserErrorTypes};
|
||||
use execution::presets;
|
||||
use grammar::grammar;
|
||||
use lalrpop_util::ParseError;
|
||||
|
||||
pub struct Parsers {}
|
||||
|
||||
@ -124,9 +125,10 @@ where
|
||||
T: Display,
|
||||
{
|
||||
match e {
|
||||
| ParseError::ExtraToken { token: (l, t, r) } =>
|
||||
Err(format!("Unexpected extra token \"{t}\" between positions {l} \
|
||||
and {r}.")),
|
||||
| ParseError::ExtraToken { token: (l, t, r) } => Err(format!(
|
||||
"Unexpected extra token \"{t}\" between positions {l} \
|
||||
and {r}."
|
||||
)),
|
||||
| ParseError::UnrecognizedEof {
|
||||
location: _,
|
||||
expected: _,
|
||||
@ -136,13 +138,13 @@ where
|
||||
| ParseError::UnrecognizedToken {
|
||||
token: (l, t, r),
|
||||
expected,
|
||||
} => {
|
||||
create_error(input_str, l, t, r, Some(expected), None)
|
||||
},
|
||||
} => create_error(input_str, l, t, r, Some(expected), None),
|
||||
| ParseError::User {
|
||||
error: UserError { token: (l, t, r), error }
|
||||
} => {
|
||||
create_error(input_str, l, t, r, None, Some(error))
|
||||
},
|
||||
error:
|
||||
UserError {
|
||||
token: (l, t, r),
|
||||
error,
|
||||
},
|
||||
} => create_error(input_str, l, t, r, None, Some(error)),
|
||||
}
|
||||
}
|
||||
|
||||
@ -3,9 +3,8 @@
|
||||
// -----------------------------------------------------------------------------
|
||||
use std::fmt;
|
||||
|
||||
use rsprocess::translator::{
|
||||
Formatter, PrintableWithTranslator, Translator,
|
||||
};
|
||||
use rsprocess::translator::{Formatter, PrintableWithTranslator, Translator};
|
||||
|
||||
use super::dsl::*;
|
||||
|
||||
impl<S> fmt::Debug for Assert<S>
|
||||
|
||||
@ -1,8 +1,9 @@
|
||||
use std::collections::HashMap;
|
||||
|
||||
use super::dsl::*;
|
||||
use rsprocess::{graph, label, set, system, translator};
|
||||
use rsprocess::translator::PrintableWithTranslator;
|
||||
use rsprocess::{graph, label, set, system, translator};
|
||||
|
||||
use super::dsl::*;
|
||||
|
||||
// ----------------------------------------------------------------------------
|
||||
// Specific Assert Implementation
|
||||
|
||||
@ -1,4 +1,5 @@
|
||||
use rsprocess::{environment, label, process, set, system, translator};
|
||||
|
||||
use super::dsl::*;
|
||||
use super::rsassert::*;
|
||||
|
||||
|
||||
@ -1,8 +1,8 @@
|
||||
use rsprocess::translator;
|
||||
use rsprocess::system::System;
|
||||
use rsprocess::label::Label;
|
||||
use petgraph::{Directed, Graph};
|
||||
use rsprocess::graph::SystemGraph;
|
||||
use petgraph::{Graph, Directed};
|
||||
use rsprocess::label::Label;
|
||||
use rsprocess::system::System;
|
||||
use rsprocess::translator;
|
||||
|
||||
// -----------------------------------------------------------------------------
|
||||
// helper functions
|
||||
@ -19,10 +19,7 @@ where
|
||||
&self,
|
||||
edge_map: &assert::relabel::Assert,
|
||||
translator: &mut translator::Translator,
|
||||
) -> Result<
|
||||
Graph<System, assert::relabel::AssertReturnValue, Ty, Ix>,
|
||||
String,
|
||||
>;
|
||||
) -> Result<Graph<System, assert::relabel::AssertReturnValue, Ty, Ix>, String>;
|
||||
}
|
||||
|
||||
impl<'a> MapEdges<'a, System, Label, Directed, u32> for SystemGraph {
|
||||
|
||||
@ -5,13 +5,13 @@ use std::rc::Rc;
|
||||
use std::{env, fs, io};
|
||||
|
||||
use petgraph::Graph;
|
||||
|
||||
use crate::data::MapEdges;
|
||||
use rsprocess::set::Set;
|
||||
use rsprocess::system::ExtensionsSystem;
|
||||
use rsprocess::translator::Translator;
|
||||
use rsprocess::*;
|
||||
|
||||
use crate::data::MapEdges;
|
||||
|
||||
// -----------------------------------------------------------------------------
|
||||
|
||||
pub trait FileParsers {
|
||||
@ -91,11 +91,11 @@ pub enum Instruction {
|
||||
so: SaveOptions,
|
||||
},
|
||||
Target {
|
||||
so: SaveOptions,
|
||||
so: SaveOptions,
|
||||
limit: Option<usize>,
|
||||
},
|
||||
Run {
|
||||
so: SaveOptions,
|
||||
so: SaveOptions,
|
||||
limit: Option<usize>,
|
||||
},
|
||||
Loop {
|
||||
@ -150,9 +150,9 @@ impl System {
|
||||
|
||||
#[derive(Clone)]
|
||||
pub struct EvaluatedSystem {
|
||||
sys: Option<system::System>,
|
||||
graph: Option<graph::SystemGraph>,
|
||||
positive: Option<system::PositiveSystem>,
|
||||
sys: Option<system::System>,
|
||||
graph: Option<graph::SystemGraph>,
|
||||
positive: Option<system::PositiveSystem>,
|
||||
translator: Translator,
|
||||
}
|
||||
|
||||
@ -163,16 +163,23 @@ impl EvaluatedSystem {
|
||||
|
||||
pub fn from_graph(
|
||||
graph: graph::SystemGraph,
|
||||
translator: Translator
|
||||
) -> Self {
|
||||
Self { sys: None, graph: Some(graph), positive: None, translator }
|
||||
}
|
||||
|
||||
pub fn from_sys(
|
||||
sys: system::System,
|
||||
translator: Translator,
|
||||
) -> Self {
|
||||
Self { sys: Some(sys), graph: None, positive: None, translator }
|
||||
Self {
|
||||
sys: None,
|
||||
graph: Some(graph),
|
||||
positive: None,
|
||||
translator,
|
||||
}
|
||||
}
|
||||
|
||||
pub fn from_sys(sys: system::System, translator: Translator) -> Self {
|
||||
Self {
|
||||
sys: Some(sys),
|
||||
graph: None,
|
||||
positive: None,
|
||||
translator,
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
@ -269,7 +276,7 @@ pub fn stats(system: &EvaluatedSystem) -> Result<String, String> {
|
||||
/// Equivalent to main_do(target, E)
|
||||
pub fn target(
|
||||
system: &EvaluatedSystem,
|
||||
limit: Option<usize>
|
||||
limit: Option<usize>,
|
||||
) -> Result<String, String> {
|
||||
if let Some(sys) = &system.sys {
|
||||
let res = if let Some(limit) = limit {
|
||||
@ -318,7 +325,7 @@ pub fn target(
|
||||
/// equivalent to main_do(run,Es)
|
||||
pub fn traversed(
|
||||
system: &EvaluatedSystem,
|
||||
limit: Option<usize>
|
||||
limit: Option<usize>,
|
||||
) -> Result<String, String> {
|
||||
let mut output = String::new();
|
||||
|
||||
@ -492,7 +499,7 @@ pub fn limit_freq<F>(
|
||||
parser_experiment: F,
|
||||
) -> Result<String, String>
|
||||
where
|
||||
F: Fn(&mut Translator, String) -> Result<(Vec<u32>, Vec<Set>), String>
|
||||
F: Fn(&mut Translator, String) -> Result<(Vec<u32>, Vec<Set>), String>,
|
||||
{
|
||||
use frequency::BasicFrequency;
|
||||
|
||||
@ -568,7 +575,7 @@ pub fn fast_freq<F>(
|
||||
parser_experiment: F,
|
||||
) -> Result<String, String>
|
||||
where
|
||||
F: Fn(&mut Translator, String) -> Result<(Vec<u32>, Vec<Set>), String>
|
||||
F: Fn(&mut Translator, String) -> Result<(Vec<u32>, Vec<Set>), String>,
|
||||
{
|
||||
use frequency::BasicFrequency;
|
||||
|
||||
@ -623,10 +630,14 @@ where
|
||||
/// Computes the LTS.
|
||||
/// equivalent to main_do(digraph, Arcs) or to main_do(advdigraph, Arcs)
|
||||
pub fn digraph(system: &mut EvaluatedSystem) -> Result<(), String> {
|
||||
if let Some(sys) = &system.sys && system.graph.is_none() {
|
||||
if let Some(sys) = &system.sys
|
||||
&& system.graph.is_none()
|
||||
{
|
||||
let graph = sys.digraph()?;
|
||||
system.graph = Some(graph);
|
||||
} else if let Some(positive) = &system.positive && system.graph.is_none() {
|
||||
} else if let Some(positive) = &system.positive
|
||||
&& system.graph.is_none()
|
||||
{
|
||||
let _graph = positive.digraph()?;
|
||||
todo!()
|
||||
}
|
||||
@ -694,25 +705,26 @@ pub fn bisimilar<F>(
|
||||
system_a: &mut EvaluatedSystem,
|
||||
edge_relabeler: &assert::relabel::Assert,
|
||||
system_b: String,
|
||||
parser_instructions: F
|
||||
parser_instructions: F,
|
||||
) -> Result<String, String>
|
||||
where
|
||||
F: Fn(&mut Translator, String) -> Result<Instructions, String>
|
||||
F: Fn(&mut Translator, String) -> Result<Instructions, String>,
|
||||
{
|
||||
use assert::relabel::AssertReturnValue;
|
||||
|
||||
let system_b = read_file(&mut system_a.translator,
|
||||
system_b.to_string(),
|
||||
parser_instructions)?;
|
||||
let system_b = read_file(
|
||||
&mut system_a.translator,
|
||||
system_b.to_string(),
|
||||
parser_instructions,
|
||||
)?;
|
||||
|
||||
let mut system_b = system_b
|
||||
.system
|
||||
.compute(system_a.get_translator().clone())?;
|
||||
let mut system_b =
|
||||
system_b.system.compute(system_a.get_translator().clone())?;
|
||||
|
||||
if system_b.translator != system_a.translator {
|
||||
return Err("Bisimilarity not implemented for systems with different \
|
||||
encodings. Serialize the systems with the same translator."
|
||||
.into());
|
||||
.into());
|
||||
}
|
||||
|
||||
digraph(system_a)?;
|
||||
@ -720,11 +732,16 @@ where
|
||||
|
||||
// since we ran digraph on both they have to have valid graphs
|
||||
|
||||
let a: Graph<system::System, AssertReturnValue> =
|
||||
system_a.graph.as_ref().unwrap()
|
||||
let a: Graph<system::System, AssertReturnValue> = system_a
|
||||
.graph
|
||||
.as_ref()
|
||||
.unwrap()
|
||||
.map_edges(edge_relabeler, &mut system_a.translator)?;
|
||||
let b: Graph<system::System, AssertReturnValue> =
|
||||
system_b.graph.unwrap().map_edges(edge_relabeler, &mut system_b.translator)?;
|
||||
system_b
|
||||
.graph
|
||||
.unwrap()
|
||||
.map_edges(edge_relabeler, &mut system_b.translator)?;
|
||||
Ok(format!(
|
||||
"{}",
|
||||
// bisimilarity::bisimilarity_kanellakis_smolka::bisimilarity(&
|
||||
@ -897,10 +914,16 @@ fn execute<P: FileParsers>(
|
||||
save_options!(freq(system)?, so);
|
||||
},
|
||||
| Instruction::LimitFrequency { experiment, so } => {
|
||||
save_options!(limit_freq(system, experiment, P::parse_experiment)?, so);
|
||||
save_options!(
|
||||
limit_freq(system, experiment, P::parse_experiment)?,
|
||||
so
|
||||
);
|
||||
},
|
||||
| Instruction::FastFrequency { experiment, so } => {
|
||||
save_options!(fast_freq(system, experiment, P::parse_experiment)?, so);
|
||||
save_options!(
|
||||
fast_freq(system, experiment, P::parse_experiment)?,
|
||||
so
|
||||
);
|
||||
},
|
||||
| Instruction::Digraph { group, gso } => {
|
||||
digraph(system)?;
|
||||
@ -940,7 +963,15 @@ fn execute<P: FileParsers>(
|
||||
so,
|
||||
} => {
|
||||
edge_relabeler.typecheck()?;
|
||||
save_options!(bisimilar(system, &edge_relabeler, system_b, P::parse_instructions)?, so);
|
||||
save_options!(
|
||||
bisimilar(
|
||||
system,
|
||||
&edge_relabeler,
|
||||
system_b,
|
||||
P::parse_instructions
|
||||
)?,
|
||||
so
|
||||
);
|
||||
},
|
||||
}
|
||||
Ok(())
|
||||
@ -948,17 +979,13 @@ fn execute<P: FileParsers>(
|
||||
|
||||
/// Interprets file at supplied path, then executes the code specified as
|
||||
/// instructions inside the file.
|
||||
pub fn run<P: FileParsers>(
|
||||
path: String,
|
||||
) -> Result<(), String> {
|
||||
pub fn run<P: FileParsers>(path: String) -> Result<(), String> {
|
||||
let mut translator = Translator::new();
|
||||
|
||||
let Instructions {
|
||||
system,
|
||||
instructions,
|
||||
} = read_file(&mut translator,
|
||||
path,
|
||||
P::parse_instructions)?;
|
||||
} = read_file(&mut translator, path, P::parse_instructions)?;
|
||||
|
||||
let mut system = system.compute(translator)?;
|
||||
|
||||
|
||||
@ -8,13 +8,18 @@ pub enum UserErrorTypes {
|
||||
impl Display for UserErrorTypes {
|
||||
fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
|
||||
match self {
|
||||
Self::NumberTooBigUsize =>
|
||||
write!(f, "Specified number is too big (greater than {})",
|
||||
usize::MAX),
|
||||
Self::NumberTooBigi64 =>
|
||||
write!(f, "Specified number is too big (lesser than {} or \
|
||||
| Self::NumberTooBigUsize => write!(
|
||||
f,
|
||||
"Specified number is too big (greater than {})",
|
||||
usize::MAX
|
||||
),
|
||||
| Self::NumberTooBigi64 => write!(
|
||||
f,
|
||||
"Specified number is too big (lesser than {} or \
|
||||
greater than {})",
|
||||
i64::MIN, i64::MAX),
|
||||
i64::MIN,
|
||||
i64::MAX
|
||||
),
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
@ -5,6 +5,7 @@ pub mod user_error {
|
||||
}
|
||||
|
||||
lalrpop_util::lalrpop_mod!(
|
||||
#[allow(clippy::uninlined_format_args)] pub grammar, // name of module
|
||||
#[allow(clippy::uninlined_format_args)]
|
||||
#[allow(clippy::type_complexity)] pub grammar, // name of module
|
||||
"/grammar.rs" // location of parser
|
||||
);
|
||||
|
||||
@ -94,7 +94,6 @@ common_label!(
|
||||
.intersection(&acc)
|
||||
);
|
||||
|
||||
|
||||
// Nodes -----------------------------------------------------------------------
|
||||
|
||||
/// Helper structure that specifies what information to display for nodes.
|
||||
|
||||
@ -83,7 +83,7 @@ pub trait ExtensionsSystem: BasicSystem {
|
||||
#[allow(clippy::type_complexity)]
|
||||
fn run_separated_limit(
|
||||
&self,
|
||||
limit: usize
|
||||
limit: usize,
|
||||
) -> Result<Vec<(Self::Set, Self::Set, Self::Set)>, String>;
|
||||
|
||||
fn traces(self, n: usize) -> Result<Vec<Trace<Self::Label, Self>>, String>;
|
||||
@ -177,7 +177,9 @@ impl<T: BasicSystem> ExtensionsSystem for T {
|
||||
}
|
||||
let mut n = 1;
|
||||
let mut current = current.unwrap().1;
|
||||
while let Some((_, next)) = current.one_transition()? && n < limit {
|
||||
while let Some((_, next)) = current.one_transition()?
|
||||
&& n < limit
|
||||
{
|
||||
current = next;
|
||||
n += 1;
|
||||
}
|
||||
@ -208,7 +210,7 @@ impl<T: BasicSystem> ExtensionsSystem for T {
|
||||
/// see smartOneRunECT, smartRunECT
|
||||
fn run_separated_limit(
|
||||
&self,
|
||||
limit: usize
|
||||
limit: usize,
|
||||
) -> Result<Vec<(Self::Set, Self::Set, Self::Set)>, String> {
|
||||
let mut limit = limit;
|
||||
let mut res = vec![];
|
||||
@ -220,7 +222,9 @@ impl<T: BasicSystem> ExtensionsSystem for T {
|
||||
let (available_entities, context, t) = current.0.get_context();
|
||||
res.push((available_entities.clone(), context.clone(), t.clone()));
|
||||
let mut current = current.1;
|
||||
while let Some((label, next)) = current.one_transition()? && limit > 1 {
|
||||
while let Some((label, next)) = current.one_transition()?
|
||||
&& limit > 1
|
||||
{
|
||||
limit -= 1;
|
||||
current = next;
|
||||
let (available_entities, context, t) = label.get_context();
|
||||
|
||||
Reference in New Issue
Block a user