hoars/
lib.rs

1//! This crate provides a parser for the HOA format.
2// #![warn(missing_docs)]
3mod body;
4mod format;
5mod header;
6pub mod input;
7mod lexer;
8pub mod output;
9mod value;
10
11use biodivine_lib_bdd::{Bdd, BddPartialValuation, BddVariable, BddVariableSet};
12use std::fmt::{Debug, Display};
13
14#[derive(Debug, Clone, Hash, Eq, PartialEq)]
15pub enum AbstractLabelExpression {
16    Boolean(bool),
17    Integer(u16),
18    Negated(Box<AbstractLabelExpression>),
19    Conjunction(Vec<AbstractLabelExpression>),
20    Disjunction(Vec<AbstractLabelExpression>),
21}
22
23pub(crate) enum Atomic {
24    Positive(u16),
25    Negative(u16),
26}
27
28impl Atomic {
29    pub(crate) fn to_value(self, vars: &[BddVariable]) -> (BddVariable, bool) {
30        match self {
31            Atomic::Positive(i) => (vars[i as usize], true),
32            Atomic::Negative(i) => (vars[i as usize], false),
33        }
34    }
35}
36
37impl AbstractLabelExpression {
38    pub(crate) fn try_atom(&self) -> Option<Atomic> {
39        match self {
40            AbstractLabelExpression::Integer(i) => Some(Atomic::Positive(*i)),
41            AbstractLabelExpression::Negated(bx) => match **bx {
42                AbstractLabelExpression::Integer(i) => Some(Atomic::Negative(i)),
43                _ => None,
44            },
45            _ => None,
46        }
47    }
48    pub fn try_into_bdd(self, vs: &BddVariableSet, vars: &[BddVariable]) -> Result<Bdd, String> {
49        match self {
50            AbstractLabelExpression::Boolean(b) => Ok(match b {
51                true => vs.mk_true(),
52                false => vs.mk_false(),
53            }),
54            AbstractLabelExpression::Integer(i) => {
55                if i < vs.num_vars() {
56                    Ok(vs.mk_var(vars[i as usize]))
57                } else {
58                    Err(format!("AP identifier {i} is too high"))
59                }
60            }
61            AbstractLabelExpression::Negated(e) => Ok(e.try_into_bdd(vs, vars)?.not()),
62            AbstractLabelExpression::Conjunction(cs) => {
63                if let Some(ints) = cs.iter().map(|c| c.try_atom()).collect::<Option<Vec<_>>>() {
64                    let valuation = BddPartialValuation::from_values(
65                        &ints.into_iter().map(|a| a.to_value(vars)).collect_vec(),
66                    );
67                    Ok(vs.mk_conjunctive_clause(&valuation))
68                } else {
69                    Err(format!(
70                        "could not parse label expression conjunct {cs:?}, expected atom"
71                    ))
72                }
73            }
74            AbstractLabelExpression::Disjunction(ds) => {
75                if let Some(ints) = ds.iter().map(|c| c.try_atom()).collect::<Option<Vec<_>>>() {
76                    let valuation = BddPartialValuation::from_values(
77                        &ints.into_iter().map(|a| a.to_value(vars)).collect_vec(),
78                    );
79                    Ok(vs.mk_disjunctive_clause(&valuation))
80                } else {
81                    Err(format!(
82                        "could not parse label expression disjunct {ds:?}, expected atom"
83                    ))
84                }
85            }
86        }
87    }
88}
89
90#[derive(Debug, Clone, Hash, Eq, PartialEq)]
91pub enum LabelExpression {
92    Parsed(Bdd),
93    Abstract(AbstractLabelExpression),
94}
95
96pub const MAX_APS: usize = 8;
97
98pub fn build_vars(count: u16) -> (BddVariableSet, Vec<BddVariable>) {
99    let vs = BddVariableSet::new_anonymous(count);
100    let vars = vs.variables().into_iter().take(count as usize).collect();
101    (vs, vars)
102}
103
104pub fn first_automaton_split_position(input: &str) -> Option<usize> {
105    const ENDLEN: usize = "--END--".len();
106
107    'outer: loop {
108        if let Some(end) = input.find("--END--") {
109            if let Some(abort) = input.find("--ABORT--") {
110                if abort < end {
111                    continue 'outer;
112                }
113            }
114            return Some(end + ENDLEN);
115        } else {
116            return None;
117        }
118    }
119}
120
121pub fn parse_hoa_automata(input: &str) -> Vec<HoaAutomaton> {
122    let mut out = Vec::new();
123    for hoa_aut in input.split_inclusive("--END--") {
124        if !hoa_aut.contains("--BODY--") {
125            continue;
126        }
127        match hoa_aut.try_into() {
128            Ok(aut) => out.push(aut),
129            Err(e) => println!("Error when parsing automaton: {}", e),
130        }
131    }
132    out
133}
134
135use ariadne::{Color, Fmt, ReportKind, Source};
136
137#[allow(unused_imports)]
138use chumsky::prelude::*;
139pub use format::*;
140
141use chumsky::{prelude::Simple, Parser};
142pub use format::{
143    AcceptanceCondition, AcceptanceInfo, AcceptanceName, AcceptanceSignature, AliasName, Property,
144};
145
146pub use body::{Body, Edge, Label, State};
147pub use header::{Header, HeaderItem};
148
149use itertools::Itertools;
150use lexer::Token;
151
152/// The type of identifier used for states.
153pub type Id = u32;
154
155/// Represents the different types of error that can be encountered when parsing a [`HoaAutomaton`].
156#[derive(Debug, PartialEq, Eq, Clone)]
157pub enum FromHoaError {
158    /// The version string does not match, we only support v1.
159    UnsupportedVersion(String),
160    /// Encapsulates that an unsupported acceptance condition was used.
161    UnsupportedAcceptanceCondition,
162    /// An error occurred when parsing the acceptance condition.
163    ParseAcceptanceCondition(String),
164    /// There was an error in the body.
165    UnsupportedBody,
166    /// Lexer encountered an error, contains detailed report.
167    LexerError(String),
168    /// Parser encountered an error, contains detailed report.
169    ParserError(String),
170    /// Abort token was encountered.
171    Abort,
172}
173
174impl Display for FromHoaError {
175    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
176        match self {
177            FromHoaError::UnsupportedVersion(version) => {
178                write!(f, "Unsupported HOA version ({})", version)
179            }
180            FromHoaError::UnsupportedAcceptanceCondition => {
181                write!(f, "Unsupported acceptance condition")
182            }
183            FromHoaError::UnsupportedBody => write!(f, "Unsupported body"),
184            FromHoaError::ParseAcceptanceCondition(message) => {
185                write!(f, "Could not parse acceptance condition: {}", message)
186            }
187            FromHoaError::Abort => write!(f, "Abort token encountered"),
188            FromHoaError::LexerError(rep) => write!(f, "Lexer error: {}", rep),
189            FromHoaError::ParserError(rep) => write!(f, "Parser error: {}", rep),
190        }
191    }
192}
193
194/// Represents a parsed HOA automaton. It consists of a the version string,
195/// a [`Header`] and a [`Body`].
196/// The header contains all the information about the automaton (e.g. the number of states, the
197/// acceptance condition, aliases etc.) and the body contains the actual transitions.
198#[derive(Debug, Clone, Eq, PartialEq)]
199pub struct HoaAutomaton {
200    header: Header,
201    body: Body,
202}
203
204/// Represents an acceptance condition as it is encoded in a HOA automaton.
205pub type HoaAcceptance = (usize, AcceptanceCondition);
206
207/// Stores information on aliases, it holds a vector of pairs of alias
208/// names and label expression. This can be used to unalias an automaton.
209pub type Aliases = Vec<(AliasName, LabelExpression)>;
210
211impl HoaAutomaton {
212    /// Adds the given state.
213    pub fn add_state(&mut self, state: State) {
214        self.body.push(state);
215    }
216
217    /// Returns the version of the HOA file.
218    pub fn version(&self) -> String {
219        self.header.get_version().expect("Version must be set!")
220    }
221
222    /// Returns the header of the HOA file.
223    pub fn header(&self) -> &Header {
224        &self.header
225    }
226
227    pub fn header_mut(&mut self) -> &mut Header {
228        &mut self.header
229    }
230
231    /// Returns the body of the HOA file.
232    pub fn body(&self) -> &Body {
233        &self.body
234    }
235
236    pub fn body_mut(&mut self) -> &mut Body {
237        &mut self.body
238    }
239
240    fn from_parsed((header, body): (Header, Body)) -> Self {
241        Self::from_parts(header, body)
242    }
243
244    /// Parses a HOA automaton from a string.
245    pub fn parser() -> impl Parser<Token, Self, Error = Simple<Token>> {
246        Header::parser()
247            .then(Body::parser())
248            .then_ignore(end())
249            .map(HoaAutomaton::from_parsed)
250    }
251
252    /// Creates a new HOA automaton from the given version, header and
253    /// body. This function will also unalias the automaton.
254    pub fn from_parts(header: Header, body: Body) -> Self {
255        let mut out = Self { header, body };
256        out.body.sort_by(|x, y| x.0.cmp(&y.0));
257        out
258    }
259
260    /// Verifies that the automaton is well-formed. This means that
261    /// - the number of states is set correctly
262    /// - all states are defined exactly once
263    pub fn verify(&self) -> Result<(), String> {
264        let mut errors = Vec::new();
265        let mut states = Vec::new();
266        for state in self.body().iter() {
267            if states.contains(&state.id()) {
268                errors.push(format!("State {} is defined more than once!", state.id()));
269            }
270            states.push(state.id());
271        }
272        if let Some(num_states) = self.num_states() {
273            if states.len() != num_states {
274                errors.push(format!(
275                    "The number of states is set to {} but there are {} states!",
276                    num_states,
277                    states.len()
278                ));
279            }
280        }
281        if errors.is_empty() {
282            Ok(())
283        } else {
284            Err(errors.join("\n"))
285        }
286    }
287
288    /// Returns the number of states in the automaton.
289    pub fn num_states(&self) -> Option<usize> {
290        debug_assert!(
291            self.header()
292                .iter()
293                .filter(|item| matches!(item, HeaderItem::States(_)))
294                .count()
295                == 1,
296            "The number of states must be set exactly once!"
297        );
298        self.header().iter().find_map(|item| match item {
299            HeaderItem::States(id) => Some(*id as usize),
300            _ => None,
301        })
302    }
303
304    /// Returns the number of edges in the automaton.
305    pub fn start(&self) -> Vec<&StateConjunction> {
306        debug_assert!(
307            self.header()
308                .iter()
309                .filter(|item| matches!(item, HeaderItem::Start(_)))
310                .count()
311                >= 1,
312            "At least one initial state conjunction has to be present!"
313        );
314        self.header()
315            .iter()
316            .filter_map(|item| match item {
317                HeaderItem::Start(start) => Some(start),
318                _ => None,
319            })
320            .collect()
321    }
322
323    /// Returns the set of all atomic propositions in the automaton.
324    pub fn aps(&self) -> &Vec<String> {
325        let aps = self
326            .header()
327            .iter()
328            .filter_map(|item| match item {
329                HeaderItem::AP(ap) => Some(ap),
330                _ => None,
331            })
332            .collect_vec();
333        debug_assert!(aps.len() == 1, "There must be exactly one AP header!");
334        aps.first().unwrap()
335    }
336
337    /// Counts the number of atomic propositions in the automaton.
338    pub fn num_aps(&self) -> usize {
339        self.aps().len()
340    }
341
342    /// Returns the acceptance condition of the automaton.
343    pub fn acceptance(&self) -> HoaAcceptance {
344        debug_assert!(
345            self.header()
346                .iter()
347                .filter(|item| matches!(item, HeaderItem::Acceptance(..)))
348                .count()
349                == 1,
350            "There must be exactly one Acceptance header!"
351        );
352        self.header()
353            .iter()
354            .find_map(|item| match item {
355                HeaderItem::Acceptance(acceptance_sets, condition) => {
356                    Some((*acceptance_sets as usize, condition.clone()))
357                }
358                _ => None,
359            })
360            .expect("Acceptance header is missing!")
361    }
362
363    /// Returns the aliases of the automaton.
364    pub fn aliases(&self) -> Vec<(AliasName, AbstractLabelExpression)> {
365        self.header()
366            .iter()
367            .filter_map(|item| match item {
368                HeaderItem::Alias(name, expr) => Some((name.clone(), expr.clone())),
369                _ => None,
370            })
371            .collect()
372    }
373
374    /// Returns the acceptance name of the automaton.
375    pub fn acceptance_name(&self) -> Option<(&AcceptanceName, &Vec<AcceptanceInfo>)> {
376        debug_assert!(
377            self.header()
378                .iter()
379                .filter(|item| matches!(item, HeaderItem::AcceptanceName(..)))
380                .count()
381                == 1,
382            "There must be exactly one AcceptanceName header!"
383        );
384        self.header().iter().find_map(|item| match item {
385            HeaderItem::AcceptanceName(name, info) => Some((name, info)),
386            _ => None,
387        })
388    }
389
390    /// Adds a header item to the automaton.
391    pub fn add_header_item(&mut self, item: HeaderItem) {
392        self.header.push(item);
393    }
394}
395
396impl Default for HoaAutomaton {
397    fn default() -> Self {
398        HoaAutomaton::from_parts(vec![HeaderItem::Version("v1".into())].into(), vec![].into())
399    }
400}
401
402impl TryFrom<&str> for HoaAutomaton {
403    type Error = FromHoaError;
404
405    fn try_from(value: &str) -> Result<Self, Self::Error> {
406        input::from_hoa(value)
407    }
408}
409
410impl std::fmt::Display for AbstractLabelExpression {
411    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
412        match self {
413            AbstractLabelExpression::Boolean(b) => match b {
414                true => write!(f, "t"),
415                false => write!(f, "f"),
416            },
417            AbstractLabelExpression::Integer(i) => write!(f, "{i}"),
418            AbstractLabelExpression::Negated(expr) => {
419                write!(f, "!{}", expr)
420            }
421            AbstractLabelExpression::Conjunction(conjuncts) => {
422                let mut it = conjuncts.iter();
423                if let Some(first) = it.next() {
424                    Display::fmt(first, f)?;
425                }
426                for succ in it {
427                    write!(f, " & ")?;
428                    Display::fmt(succ, f)?;
429                }
430                Ok(())
431            }
432            AbstractLabelExpression::Disjunction(disjuncts) => {
433                let mut it = disjuncts.iter();
434                if let Some(first) = it.next() {
435                    Display::fmt(first, f)?;
436                }
437                for succ in it {
438                    write!(f, " | ")?;
439                    Display::fmt(succ, f)?;
440                }
441                Ok(())
442            }
443        }
444    }
445}
446
447fn build_error_report<I: Iterator<Item = Simple<String>>>(input: &str, errs: I) -> String {
448    errs.into_iter()
449        .map(|e| {
450            let report = ariadne::Report::build(ReportKind::Error, (), e.span().start);
451
452            let report = match e.reason() {
453                chumsky::error::SimpleReason::Unexpected => report
454                    .with_message(format!(
455                        "{}, expected {}",
456                        if e.found().is_some() {
457                            "Unexpected token in input"
458                        } else {
459                            "Unexpected end of input"
460                        },
461                        if e.expected().len() == 0 {
462                            "something else".to_string()
463                        } else {
464                            e.expected()
465                                .map(|expected| match expected {
466                                    Some(expected) => expected.to_string(),
467                                    None => "end of input".to_string(),
468                                })
469                                .collect::<Vec<_>>()
470                                .join(", ")
471                        }
472                    ))
473                    .with_label(
474                        ariadne::Label::new(e.span())
475                            .with_message(format!(
476                                "Unexpected token {}",
477                                e.found()
478                                    .unwrap_or(&"end of file".to_string())
479                                    .fg(Color::Red)
480                            ))
481                            .with_color(Color::Red),
482                    ),
483                chumsky::error::SimpleReason::Unclosed { span, delimiter } => report
484                    .with_message(format!(
485                        "Unclosed delimiter {}",
486                        delimiter.fg(Color::Yellow)
487                    ))
488                    .with_label(
489                        ariadne::Label::new(span.clone())
490                            .with_message(format!(
491                                "Unclosed delimiter {}",
492                                delimiter.fg(Color::Yellow)
493                            ))
494                            .with_color(Color::Yellow),
495                    )
496                    .with_label(
497                        ariadne::Label::new(e.span())
498                            .with_message(format!(
499                                "Must be closed before this {}",
500                                e.found()
501                                    .unwrap_or(&"end of file".to_string())
502                                    .fg(Color::Red)
503                            ))
504                            .with_color(Color::Red),
505                    ),
506                chumsky::error::SimpleReason::Custom(msg) => report.with_message(msg).with_label(
507                    ariadne::Label::new(e.span())
508                        .with_message(format!("{}", msg.fg(Color::Red)))
509                        .with_color(Color::Red),
510                ),
511            };
512
513            let mut report_output = Vec::new();
514            report
515                .finish()
516                .write(Source::from(input), &mut report_output)
517                .unwrap();
518
519            std::str::from_utf8(&report_output)
520                .unwrap_or("Could not parse error report")
521                .to_string()
522        })
523        .join("\n")
524}
525
526#[cfg(test)]
527fn print_error_report<I: Iterator<Item = Simple<String>>>(input: &str, errs: I) {
528    eprintln!("{}", build_error_report(input, errs))
529}
530
531#[cfg(test)]
532mod tests {
533    use crate::{
534        body::{Edge, State},
535        header::Header,
536        AcceptanceAtom, AcceptanceCondition, AcceptanceName, AcceptanceSignature, Body, HeaderItem,
537        HoaAutomaton, Label, StateConjunction, ALPHABET, VARS,
538    };
539
540    #[test]
541    fn first_automaton_split_and_abort() {
542        let contents = "HOA: v1\n--END--\nHOA: v1\n--ABORT--\nHOA: v1\n--END--\n";
543
544        let first = super::first_automaton_split_position(contents);
545        assert_eq!(first, Some(15));
546    }
547
548    #[test]
549    fn real_test_1() {
550        let contents = r#"HOA: v1
551             AP: 1 "a"
552             States: 3
553             Start: 0
554             acc-name: Buchi
555             Acceptance: 1 Inf(0)
556             --BODY--
557             State: 0 {0}
558              [0] 1
559              [!0]  2
560             State: 1  /* former state 0 */
561              [0] 1
562              [!0] 2
563             State: 2  /* former state 1 */
564              [0] 1
565              [!0] 2
566             --END--
567             "#;
568        let hoa_aut = HoaAutomaton::try_from(contents);
569
570        if let Err(err) = hoa_aut {
571            println!("Encountered paring error\n{}", err);
572            return;
573        }
574
575        let header = Header::from_vec(vec![
576            HeaderItem::Version("v1".to_string()),
577            HeaderItem::AP(vec!["a".to_string()]),
578            HeaderItem::States(3),
579            HeaderItem::Start(StateConjunction(vec![0])),
580            HeaderItem::AcceptanceName(AcceptanceName::Buchi, vec![]),
581            HeaderItem::Acceptance(1, AcceptanceCondition::Inf(AcceptanceAtom::Positive(0))),
582        ]);
583        let q0 = State::from_parts(
584            0,
585            None,
586            vec![
587                Edge::from_parts(
588                    Label(ALPHABET.mk_var(VARS[0])),
589                    StateConjunction(vec![1]),
590                    AcceptanceSignature(vec![0]),
591                ),
592                Edge::from_parts(
593                    Label(ALPHABET.mk_var(VARS[0]).not()),
594                    StateConjunction(vec![2]),
595                    AcceptanceSignature(vec![0]),
596                ),
597            ],
598        );
599        let q1 = State::from_parts(
600            1,
601            None,
602            vec![
603                Edge::from_parts(
604                    Label(ALPHABET.mk_var(VARS[0])),
605                    StateConjunction(vec![1]),
606                    AcceptanceSignature(vec![]),
607                ),
608                Edge::from_parts(
609                    Label(ALPHABET.mk_var(VARS[0]).not()),
610                    StateConjunction(vec![2]),
611                    AcceptanceSignature(vec![]),
612                ),
613            ],
614        );
615        let q2 = State::from_parts(
616            2,
617            None,
618            vec![
619                Edge::from_parts(
620                    Label(ALPHABET.mk_var(VARS[0])),
621                    StateConjunction(vec![1]),
622                    AcceptanceSignature(vec![]),
623                ),
624                Edge::from_parts(
625                    Label(ALPHABET.mk_var(VARS[0]).not()),
626                    StateConjunction(vec![2]),
627                    AcceptanceSignature(vec![]),
628                ),
629            ],
630        );
631        assert_eq!(
632            hoa_aut,
633            Ok(HoaAutomaton::from_parts(
634                header,
635                Body::from(vec![q0, q1, q2])
636            ))
637        )
638    }
639}
hoars/lib.rs

hoars/
lib.rs
