Support output state based acceptance automata

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--

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<Option<Id>> {
-        if self.len() == 0 {
+        if self.is_empty() {
             Some(None)
         } else if self.len() == 1 {
             Some(Some(self[0]))

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}"));
+    }
 }

src/output.rs

@@ -1,18 +1,28 @@
-use std::fmt::Display;
-
 use itertools::Itertools;
+use std::fmt::{Display, Write};
 
 use crate::{
     AcceptanceAtom, AcceptanceCondition, AcceptanceInfo, AcceptanceName, AcceptanceSignature,
     AliasName, Edge, HeaderItem, HoaAutomaton, HoaBool, Label, Property, State, StateConjunction,
 };
 
 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
+    }
+}

src/value.rs

@@ -63,7 +63,7 @@ pub fn acceptance_info() -> impl Parser<Token, AcceptanceInfo, Error = Simple<To
 pub fn label_expression() -> impl Parser<Token, AbstractLabelExpression, Error = Simple<Token>> {
     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))));