diff --git a/hoa/stateacc.hoa b/hoa/stateacc.hoa new file mode 100644 index 0000000..1b081d6 --- /dev/null +++ b/hoa/stateacc.hoa @@ -0,0 +1,19 @@ +HOA: v1 +States: 10 +Start: 0 +AP: 2 "p0" "p1" +acc-name: Buchi +Acceptance: 1 Inf(0) +properties: trans-labels explicit-labels state-acc +--BODY-- +State: 0 +[!0&!1] 1 +[ 0&!1] 1 +[ !0&1] 1 +[0 & 1] 0 +State: 1 {0} +[!0&!1] 0 +[ 0&!1] 0 +[!0& 1] 1 +[ 0 &1] 1 +--END-- diff --git a/src/format.rs b/src/format.rs index ef14534..d921614 100644 --- a/src/format.rs +++ b/src/format.rs @@ -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> { - if self.len() == 0 { + if self.is_empty() { Some(None) } else if self.len() == 1 { Some(Some(self[0])) diff --git a/src/lib.rs b/src/lib.rs index cef3473..fbc3528 100644 --- a/src/lib.rs +++ b/src/lib.rs @@ -533,6 +533,7 @@ mod tests { use crate::{ body::{Edge, State}, header::Header, + output::to_hoa, AcceptanceAtom, AcceptanceCondition, AcceptanceName, AcceptanceSignature, Body, HeaderItem, HoaAutomaton, Label, StateConjunction, ALPHABET, VARS, }; @@ -636,4 +637,12 @@ mod tests { )) ) } + + #[test] + fn real_test_state_acc() { + let contents = include_str!("../hoa/stateacc.hoa"); + let hoa_aut = HoaAutomaton::try_from(contents); + let result = to_hoa(&hoa_aut.unwrap()); + assert!(result.contains("State: 1 {0}")); + } } diff --git a/src/output.rs b/src/output.rs index 5f6aebf..7443708 100644 --- a/src/output.rs +++ b/src/output.rs @@ -1,6 +1,5 @@ -use std::fmt::Display; - use itertools::Itertools; +use std::fmt::{Display, Write}; use crate::{ AcceptanceAtom, AcceptanceCondition, AcceptanceInfo, AcceptanceName, AcceptanceSignature, @@ -8,11 +7,22 @@ use crate::{ }; pub fn to_hoa(aut: &HoaAutomaton) -> String { + let state_acceptance = aut.header().iter().any(|it| { + if let HeaderItem::Properties(properties) = it { + properties.iter().contains(&Property::StateAcceptance) + } else { + false + } + }); aut.header() .into_iter() .map(|header_item| header_item.to_string()) .chain(std::iter::once("--BODY--".to_string())) - .chain(aut.body().into_iter().map(|state| state.to_string())) + .chain( + aut.body() + .into_iter() + .map(|state| state.fmt_with_config(state_acceptance)), + ) .chain(std::iter::once("--END--".to_string())) .join("\n") } @@ -181,3 +191,31 @@ impl Display for State { Ok(()) } } + +impl State { + fn fmt_with_config(&self, state_acceptance: bool) -> String { + let mut f = String::new(); + if let Some(comment) = &self.1 { + write!(f, "State: {} \"{}\"", self.0, comment).unwrap(); + } else { + write!(f, "State: {}", self.0).unwrap(); + } + if state_acceptance { + let acceptance = self.2.iter().map(|it| &it.2).all_equal_value(); + if let Ok(acceptance) = acceptance { + writeln!(f, " {acceptance}").unwrap(); + } else { + writeln!(f).unwrap(); + } + for edge in &self.2 { + writeln!(f, "{} {}", edge.0, edge.1).unwrap(); + } + } else { + writeln!(f).unwrap(); + for edge in &self.2 { + writeln!(f, "{edge}").unwrap(); + } + } + f + } +} diff --git a/src/value.rs b/src/value.rs index 938061c..fff4976 100644 --- a/src/value.rs +++ b/src/value.rs @@ -63,7 +63,7 @@ pub fn acceptance_info() -> impl Parser impl Parser> { recursive(|label_expression| { let value = boolean() - .map(|b| AbstractLabelExpression::Boolean(b)) + .map(AbstractLabelExpression::Boolean) .or(integer().map(|i| AbstractLabelExpression::Integer(i as u16))); // .or(alias_name().map(|aname| LabelExpression::Alias(AliasName(aname))));