Differences

This shows you the differences between two versions of the page.

--- complement [2018/11/12 14:37] – created liyong
+++ complement [2018/11/13 13:39] (current) – liyong
@@ Line 1: / Line 1: @@
 ====== Complementation ======
+This page shows how to use ROLL to complement a given Büchi automaton.
+Suppose the given input Büchi automaton is described in Hanoi format as follows.
+<code java>
+HOA: v1
+tool: "ROLL"
+properties: explicit-labels state-acc trans-labels
+States: 2
+Start: 0
+acc-name: Buchi
+Acceptance: 1 Inf(0)
+AP: 1 "b"
+--BODY--
+State: 0
+  [!0] 0
+  [0] 0
+  [0] 1
+State: 1 {0}
+  [0] 1
+--END--
+</code>
+This Büchi automaton is the smallest automaton recognizing the language specified by the LTL formula "F (G b)".
+As an example, one can use following command line to complement the given automaton.
+<code>
+java -jar ROLL.jar complement A.hoa -table -syntactic
+</code>
+It will give us a complement automaton described in the Hanoi format as follows.
+<code java>
+HOA: v1
+tool: "ROLL"
+properties: explicit-labels state-acc trans-labels
+States: 4
+Start: 0
+acc-name: Buchi
+Acceptance: 1 Inf(0)
+AP: 1 "b"
+--BODY--
+State: 0
+[(!0)]  0
+[(!0)]  1
+[(!0)]  2
+[(0)]  0
+[(0)]  3
+State: 1
+[(!0)]  1
+[(!0)]  2
+[(0)]  1
+[(0)]  2
+State: 2 {0}
+[(!0)]  1
+[(0)]  3
+State: 3
+[(!0)]  1
+[(!0)]  2
+[(0)]  3
+--END--
+</code>
+The complete log information is the following.
+<code>
+/11/12 14:46:35 [ info] ROLL for BA complementation...
+HOA: v1
+tool: "ROLL"
+properties: explicit-labels state-acc trans-labels
+States: 2
+Start: 0
+acc-name: Buchi
+Acceptance: 1 Inf(0)
+AP: 1 "b"
+--BODY--
+State: 0
+[(!0)]  0
+[(0)]  0
+[(0)]  1
+State: 1 {0}
+[(0)]  1
+--END--
+HOA: v1
+tool: "ROLL"
+properties: explicit-labels state-acc trans-labels
+States: 4
+Start: 0
+acc-name: Buchi
+Acceptance: 1 Inf(0)
+AP: 1 "b"
+--BODY--
+State: 0
+[(!0)]  0
+[(!0)]  1
+[(!0)]  2
+[(0)]  0
+[(0)]  3
+State: 1
+[(!0)]  1
+[(!0)]  2
+[(0)]  1
+[(0)]  2
+State: 2 {0}
+[(!0)]  1
+[(0)]  3
+State: 3
+[(!0)]  1
+[(!0)]  2
+[(0)]  3
+--END--
+  #LT = 2                            // #number of letters
+  #T.S = 2                           // #states of target
+  #T.T = 4                           // #transitions of target
+  #H.S = 4                           // #states of learned automaton
+  #H.T = 14                          // #transitions of learned automaton
+  #L.S = 1                           // #states of leading automaton or L$
+  #P.S = [2, ]                       // #states of each progress automaton
+  #F.S = 3                           // #L.S + #P.S
+  #MQ = 4                            // #membership query
+  #EQ = 1                            // #equivalence query
+  #TMQ = 3 (ms)                      // time for membership queries
+  #TEQ = 34 (ms)                     // time for equivalence queries
+  #TLEQ = 34 (ms)                    // time for the last equivalence query
+  #TTR = 0 (ms)                      // time for the translator
+  #TLR = 16 (ms)                     // time for the learner
+  #TLRL = 5 (ms)                     // time for the learning leading automaton
+  #TLRP = 5 (ms)                     // time for the learning progress automata
+  #TTO = 147 (ms)                    // total time for learning Buchi automata
+</code>