Adding traces
This commit is contained in:
@ -41,7 +41,7 @@ impl From<Vec<IdType>> for RSset {
|
|||||||
}
|
}
|
||||||
|
|
||||||
impl RSset {
|
impl RSset {
|
||||||
pub fn new() -> Self {
|
pub const fn new() -> Self {
|
||||||
RSset {
|
RSset {
|
||||||
identifiers: BTreeSet::new(),
|
identifiers: BTreeSet::new(),
|
||||||
}
|
}
|
||||||
|
|||||||
@ -160,3 +160,70 @@ pub fn run_separated(
|
|||||||
}
|
}
|
||||||
Ok(res)
|
Ok(res)
|
||||||
}
|
}
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
fn nth_transition(
|
||||||
|
system: &RSsystem,
|
||||||
|
n: usize,
|
||||||
|
) -> Result<Option<(RSlabel, RSsystem)>, String> {
|
||||||
|
let mut tr = TransitionsIterator::from(system)?;
|
||||||
|
Ok(tr.nth(n))
|
||||||
|
}
|
||||||
|
|
||||||
|
type Trace = Vec<(Option<Rc<RSlabel>>, Rc<RSsystem>)>;
|
||||||
|
|
||||||
|
pub fn traces(
|
||||||
|
system: RSsystem,
|
||||||
|
n: usize,
|
||||||
|
) -> Result<Vec<Trace>, String> {
|
||||||
|
if n == 0 {
|
||||||
|
return Ok(vec![])
|
||||||
|
}
|
||||||
|
|
||||||
|
let mut n = n;
|
||||||
|
let mut res : Vec<Trace> = vec![];
|
||||||
|
let mut current_trace: Trace = vec![(None, Rc::new(system))];
|
||||||
|
let mut branch = vec![0];
|
||||||
|
let mut depth = 0;
|
||||||
|
let mut new_branch = true;
|
||||||
|
|
||||||
|
loop {
|
||||||
|
let next_sys = nth_transition(¤t_trace[depth].1,
|
||||||
|
branch[depth])?;
|
||||||
|
|
||||||
|
if let Some((current_label, next_sys)) = next_sys {
|
||||||
|
depth += 1;
|
||||||
|
if depth >= branch.len() {
|
||||||
|
branch.push(0);
|
||||||
|
current_trace.push((Some(Rc::new(current_label)),
|
||||||
|
Rc::new(next_sys)));
|
||||||
|
} else {
|
||||||
|
branch[depth] = 0;
|
||||||
|
current_trace[depth] = (Some(Rc::new(current_label)),
|
||||||
|
Rc::new(next_sys));
|
||||||
|
}
|
||||||
|
new_branch = true;
|
||||||
|
} else {
|
||||||
|
// at the bottom of a trace, we save to res, then backtrack until
|
||||||
|
// we find another possible path.
|
||||||
|
if new_branch {
|
||||||
|
res.push(current_trace[0..depth].to_vec());
|
||||||
|
new_branch = false;
|
||||||
|
n -= 1;
|
||||||
|
}
|
||||||
|
if n == 0 {
|
||||||
|
break;
|
||||||
|
}
|
||||||
|
|
||||||
|
if depth == 0 {
|
||||||
|
break;
|
||||||
|
}
|
||||||
|
|
||||||
|
depth -= 1;
|
||||||
|
branch[depth] += 1;
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
Ok(res)
|
||||||
|
}
|
||||||
|
|||||||
Reference in New Issue
Block a user