Skip to content
Open
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension


Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
10 changes: 5 additions & 5 deletions Cargo.toml
Original file line number Diff line number Diff line change
Expand Up @@ -9,11 +9,11 @@ exclude = ["python", "bench"]
[workspace.dependencies]
tracing = "0.1"
tracing-subscriber = "0.3"
biodivine-lib-bdd = "0.5.23"
itertools = "0.14.0"
biodivine-lib-bdd = "0.6"
itertools = "0.14"
indexmap = "2.7"
bimap = "0.6"
rand = "0.8.5"
rand = { version = "0.10", features = ["thread_rng"] }
thiserror = "2.0"
crossbeam-channel = "0.5.14"
tabled = { version = "0.16", features = ["ansi"] }
crossbeam-channel = "0.5"
tabled = { version = "0.20", features = ["ansi"] }
2 changes: 1 addition & 1 deletion crates/automata-core/src/alphabet.rs
Original file line number Diff line number Diff line change
Expand Up @@ -182,7 +182,7 @@ impl<S: Symbol> Iterator for FreeMonoid<S> {
}

if carry {
self.current = std::iter::repeat(0).take(self.current.len() + 1).collect();
self.current = std::iter::repeat_n(0, self.current.len() + 1).collect();
}

Some(out)
Expand Down
2 changes: 1 addition & 1 deletion crates/automata-core/src/alphabet/propositional.rs
Original file line number Diff line number Diff line change
Expand Up @@ -111,7 +111,7 @@ impl<RawTy: RawSymbolRepr> PropSymbol<RawTy> {
BddValuation::new(self.as_bools())
}
pub fn from_bdd_valuation(val: BddValuation) -> Self {
Self::from_bools(val.vector())
Self::from_bools(val.into_vector())
}
}

Expand Down
9 changes: 8 additions & 1 deletion crates/automata-core/src/word/finite.rs
Original file line number Diff line number Diff line change
Expand Up @@ -2,7 +2,7 @@ use std::collections::VecDeque;

use itertools::Itertools;

use crate::{alphabet::Symbol, show::Show};
use crate::{alphabet::Symbol, show::Show, word::skip::Rotated};

use super::{Concat, PeriodicOmegaWord, Repeat, Word, omega::OmegaIteration};

Expand Down Expand Up @@ -78,6 +78,13 @@ pub trait FiniteWord: Word {
Repeat::new(self, times)
}

fn rotate(self, steps: usize) -> Rotated<Self>
where
Self: Sized,
{
Rotated(self, steps)
}

/// Builds the [`PeriodicOmegaWord`] word that is the omega power of this word, i.e. if
/// `self` is the word `u`, then the result is the word `u^ω` = `u u u u ...`.
/// Panics if `self` is empty as the operation is not defined in that case.
Expand Down
2 changes: 1 addition & 1 deletion crates/automata-core/src/word/omega.rs
Original file line number Diff line number Diff line change
Expand Up @@ -155,7 +155,7 @@ fn deduplicate_inplace<S: Eq>(input: &mut Vec<S>) {
for i in 1..=(input.len() / 2) {
// for a word w of length n, if th first n-i symbols of w are equal to the
// last n-i symbols of w, then w is periodic with period i
if input.len() % i == 0 && input[..input.len() - i] == input[i..] {
if input.len().is_multiple_of(i) && input[..input.len() - i] == input[i..] {
input.truncate(i);
return;
}
Expand Down
1 change: 1 addition & 0 deletions crates/automata-core/src/word/skip.rs
Original file line number Diff line number Diff line change
Expand Up @@ -56,6 +56,7 @@ impl<W: FiniteWord> Word for Rotated<W> {
}
}

#[derive(Clone, PartialEq, Debug, Hash, Eq)]
pub struct RotatedIter<'a, W> {
rotated: &'a Rotated<W>,
start: usize,
Expand Down
18 changes: 9 additions & 9 deletions crates/automata-learning/src/active/lstar.rs
Original file line number Diff line number Diff line change
Expand Up @@ -351,16 +351,16 @@ mod tests {
use automata::TransitionSystem;
use automata::automaton::{MealyMachine, MooreMachine};
use automata::core::alphabet::CharAlphabet;
use rand::Rng;
use rand::{Rng, RngExt};
use tracing::trace;

#[test]
fn lstar_random_mealy() {
let mut rng = rand::thread_rng();
let mut rng = rand::rng();
for i in 0..200 {
let symbols = rng.gen_range(1..5);
let max_color = rng.gen_range(1..10);
let size = rng.gen_range(1..25);
let symbols = rng.random_range(1..5);
let max_color = rng.random_range(1..10);
let size = rng.random_range(1..25);

let pre_gen = std::time::Instant::now();
let ts = automata::random::generate_random_mealy(symbols, max_color, size);
Expand All @@ -387,11 +387,11 @@ mod tests {
}
#[test]
fn lstar_random_moore() {
let mut rng = rand::thread_rng();
let mut rng = rand::rng();
for i in 0..200 {
let symbols = rng.gen_range(1..5);
let max_color = rng.gen_range(1..10);
let size = rng.gen_range(1..25);
let symbols = rng.random_range(1..5);
let max_color = rng.random_range(1..10);
let size = rng.random_range(1..25);

let pre_gen = std::time::Instant::now();
let ts = automata::random::generate_random_moore(symbols, max_color, size);
Expand Down
1 change: 1 addition & 0 deletions crates/automata-learning/src/passive/dpainf.rs
Original file line number Diff line number Diff line change
Expand Up @@ -316,6 +316,7 @@ pub enum DpaInfError<A: Alphabet> {
}

/// Runs the omega-sprout algorithm on a given conflict relation.
#[allow(clippy::result_large_err)]
pub fn dpainf<A, C>(
conflicts: C,
additional_constraints: Vec<Box<dyn ConsistencyCheck<A>>>,
Expand Down
1 change: 1 addition & 0 deletions crates/automata-learning/src/passive/sample/omega.rs
Original file line number Diff line number Diff line change
Expand Up @@ -188,6 +188,7 @@ impl<A: Alphabet> OmegaSample<A> {
}

/// Computes the [`RightCongruence`] underlying the sample.
#[allow(clippy::result_large_err)]
pub fn infer_prefix_congruence(&self) -> Result<RightCongruence<A>, DpaInfError<A>> {
dpainf(prefix_consistency_conflicts(self), vec![], true, None)
}
Expand Down
14 changes: 7 additions & 7 deletions crates/automata/src/automaton/omega/buchi.rs
Original file line number Diff line number Diff line change
Expand Up @@ -70,13 +70,13 @@ where
// let InfinityColors(colors) = self
// .induced(&full_word, self.initial())
// .expect("word is valid");
if let Some(infset) = self.visited_edge_colors_from(good_scc.first(), &full_word) {
if infset.iter().any(|b| *b) {
let spoke = self
.word_from_to(self.initial, good_scc.first())
.expect("We know this is reachable!");
return Some(ReducedOmegaWord::ultimately_periodic(spoke, full_word));
}
if let Some(infset) = self.visited_edge_colors_from(good_scc.first(), &full_word)
&& infset.iter().any(|b| *b)
{
let spoke = self
.word_from_to(self.initial, good_scc.first())
.expect("We know this is reachable!");
return Some(ReducedOmegaWord::ultimately_periodic(spoke, full_word));
}
// if colors.contains(&true) {
// let base = self
Expand Down
2 changes: 1 addition & 1 deletion crates/automata/src/automaton/omega/parity.rs
Original file line number Diff line number Diff line change
Expand Up @@ -51,7 +51,7 @@ where
type Output = bool;
type Observer = run::EdgeColorLimit<T>;
fn evaluate(&self, observed: <Self::Observer as run::Observer<T>>::Current) -> Self::Output {
observed % 2 == 0
observed.is_multiple_of(2)
}
}

Expand Down
22 changes: 10 additions & 12 deletions crates/automata/src/dot.rs
Original file line number Diff line number Diff line change
Expand Up @@ -216,18 +216,16 @@ pub trait Dottable: TransitionSystem {
.arg(tempfile_name)
.spawn()?;
if !child.wait()?.success() {
Err(std::io::Error::new(
std::io::ErrorKind::Other,
child
.stdout
.map_or("Error in dot...".to_string(), |mut err| {
let mut buf = String::new();
if let Err(e) = err.read_to_string(&mut buf) {
buf = format!("Could not read from stdout: {e}");
}
buf
}),
))
Err(std::io::Error::other(child.stdout.map_or(
"Error in dot...".to_string(),
|mut err| {
let mut buf = String::new();
if let Err(e) = err.read_to_string(&mut buf) {
buf = format!("Could not read from stdout: {e}");
}
buf
},
)))
} else {
Ok(())
}
Expand Down
14 changes: 7 additions & 7 deletions crates/automata/src/minimization/partition_refinement.rs
Original file line number Diff line number Diff line change
Expand Up @@ -33,13 +33,13 @@ where
for sym in mm.symbols() {
let mut splitter = math::Map::default();
for q in mm.state_indices() {
if let Some(t) = mm.edge(q, sym) {
if set.contains(&t.target()) {
splitter
.entry(t.color())
.or_insert(BTreeSet::default())
.insert(q);
}
if let Some(t) = mm.edge(q, sym)
&& set.contains(&t.target())
{
splitter
.entry(t.color())
.or_insert(BTreeSet::default())
.insert(q);
}
}

Expand Down
23 changes: 12 additions & 11 deletions crates/automata/src/random/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -7,7 +7,8 @@ use automata_core::alphabet::{Alphabet, CharAlphabet};
use automata_core::word::ReducedOmegaWord;
use automata_core::{Int, Void, math, upw};
use math::sample_continuous_bernoulli;
use rand::{Rng, rngs::ThreadRng, thread_rng};
use rand::RngExt;
use rand::{Rng, rng, rngs::ThreadRng};
use std::cmp::min;
use tracing::{debug, info};

Expand All @@ -25,7 +26,7 @@ pub fn generate_random_ts(symbols: usize, probability: f64) -> (DTS, StateIndex<

let mut current = dts.add_state(Void);
let mut symbol_position = 0;
let mut rng = thread_rng();
let mut rng = rng();

'outer: loop {
if current >= (dts.size() as DefaultIdType) {
Expand All @@ -44,7 +45,7 @@ pub fn generate_random_ts(symbols: usize, probability: f64) -> (DTS, StateIndex<
symbol_position += 1;

for target in 0..=current {
let value: f64 = rng.gen_range(0.0..=1.0);
let value: f64 = rng.random_range(0.0..=1.0);
if value < probability {
dts.add_edge((current, symbol, target));
continue 'outer;
Expand All @@ -62,7 +63,7 @@ pub fn generate_random_ts(symbols: usize, probability: f64) -> (DTS, StateIndex<
/// Works as [`generate_random_ts`], but returns a [`DFA`] instead by randomly coloring the states.
pub fn generate_random_dfa(symbols: usize, probability: f64) -> DFA {
let (ts, initial) = generate_random_ts(symbols, probability);
ts.map_state_colors(|_| thread_rng().gen_bool(probability))
ts.map_state_colors(|_| rng().random_bool(probability))
.with_initial(initial)
.into_dfa()
}
Expand All @@ -72,7 +73,7 @@ pub fn generate_random_dfa(symbols: usize, probability: f64) -> DFA {
pub fn generate_random_mealy(symbols: usize, max_color: usize, size: usize) -> MealyMachine {
let (ts, initial) = generate_random_ts_sized(symbols, size);
let mut mm = ts
.map_edge_colors(|_| thread_rng().gen_range(0..=max_color) as Int)
.map_edge_colors(|_| rng().random_range(0..=max_color) as Int)
.with_initial(initial)
.into_mealy()
.minimize()
Expand All @@ -86,7 +87,7 @@ pub fn generate_random_mealy(symbols: usize, max_color: usize, size: usize) -> M
pub fn generate_random_moore(symbols: usize, max_color: usize, size: usize) -> MooreMachine {
let (ts, initial) = generate_random_ts_sized(symbols, size);
let mut mm = ts
.map_state_colors(|_| thread_rng().gen_range(0..=max_color) as Int)
.map_state_colors(|_| rng().random_range(0..=max_color) as Int)
.with_initial(initial)
.into_moore()
.minimize()
Expand All @@ -111,10 +112,10 @@ pub fn generate_random_ts_sized(symbols: usize, size: usize) -> (DTS, StateIndex
dts.add_state(Void);
}
// add edges
let mut rng = thread_rng();
let mut rng = rng();
for q in dts.state_indices_vec() {
for sym in alphabet.universe() {
let target = rng.gen_range(0..(dts.size() as DefaultIdType));
let target = rng.random_range(0..(dts.size() as DefaultIdType));
dts.add_edge((q, sym, target));
}
}
Expand Down Expand Up @@ -165,11 +166,11 @@ pub fn draw_priority(num_prios: u8, lambda: f64) -> u8 {
pub fn generate_random_word(alphabet: &CharAlphabet, min_len: usize, max_len: usize) -> String {
let charset: Vec<char> = alphabet.universe().collect();

let mut rng = thread_rng();
let length = rng.gen_range(min_len..=max_len);
let mut rng = rng();
let length = rng.random_range(min_len..=max_len);
let random_word: String = (0..length)
.map(|_| {
let idx = rng.gen_range(0..charset.len());
let idx = rng.random_range(0..charset.len());
charset[idx] as char
})
.collect();
Expand Down
8 changes: 3 additions & 5 deletions crates/automata/src/ts/impls/linked.rs
Original file line number Diff line number Diff line change
Expand Up @@ -504,11 +504,9 @@ impl<A: Alphabet, Q: Color, C: Color, const DET: bool> Sproutable
let (q, a, c, p) = t.into_edge_tuple();

let mut out = None;
if DET {
if let Some(pos) = self.out_edge_position(q.into_usize(), &a) {
trace!("found previously existing edge {pos} in deterministic automaton");
out = Some(self.swap_remove_edge(pos).unwrap());
}
if DET && let Some(pos) = self.out_edge_position(q.into_usize(), &a) {
trace!("found previously existing edge {pos} in deterministic automaton");
out = Some(self.swap_remove_edge(pos).unwrap());
}

let mut edge = LinkedListTransitionSystemEdge::new(q, a, c, p);
Expand Down
1 change: 1 addition & 0 deletions crates/hoars/src/body.rs
Original file line number Diff line number Diff line change
Expand Up @@ -8,6 +8,7 @@ use crate::{
};

#[derive(Debug, Clone, PartialEq, Eq, Hash)]
#[allow(unused)]
pub struct Alphabet(pub Vec<AtomicProposition>);

#[derive(Clone, Debug)]
Expand Down
2 changes: 1 addition & 1 deletion crates/hoars/src/format.rs
Original file line number Diff line number Diff line change
Expand Up @@ -55,7 +55,7 @@ impl AcceptanceSignature {
/// Tries to get the singleton element of the acceptance signature, if it exists.
/// Returns `None` if the acceptance signature is not a singleton.
pub fn get_singleton(&self) -> Option<Option<Id>> {
if self.len() == 0 {
if self.is_empty() {
Some(None)
} else if self.len() == 1 {
Some(Some(self[0]))
Expand Down
24 changes: 12 additions & 12 deletions crates/hoars/src/lib.rs
Original file line number Diff line number Diff line change
Expand Up @@ -155,14 +155,14 @@ impl HoaRepresentation {
}
states.push(state.id());
}
if let Some(num_states) = self.num_states() {
if states.len() != num_states {
errors.push(format!(
"The number of states is set to {} but there are {} states!",
num_states,
states.len()
));
}
if let Some(num_states) = self.num_states()
&& states.len() != num_states
{
errors.push(format!(
"The number of states is set to {} but there are {} states!",
num_states,
states.len()
));
}
if errors.is_empty() {
Ok(())
Expand Down Expand Up @@ -422,10 +422,10 @@ pub fn first_automaton_split_position(input: &str) -> Option<usize> {

'outer: loop {
if let Some(end) = input.find("--END--") {
if let Some(abort) = input.find("--ABORT--") {
if abort < end {
continue 'outer;
}
if let Some(abort) = input.find("--ABORT--")
&& abort < end
{
continue 'outer;
}
return Some(end + ENDLEN);
} else {
Expand Down
Loading