Differences

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

--- complement [2018/11/12 14:45] – liyong
+++ complement [2018/11/13 13:39] (current) – liyong
@@ Line 20: / Line 20: @@
 --END--
 </code>
-This Büchi automaton is the smallest automaton to recognize the language specified by the LTL formula "F G b".
+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:41:08 [ info] ROLL for BA complementation...
+/11/12 14:46:35 [ info] ROLL for BA complementation...
 HOA: v1
 tool: "ROLL"
@@ Line 79: / Line 115: @@
   #MQ = 4                            // #membership query
   #EQ = 1                            // #equivalence query
-  #TMQ = 5 (ms)                      // time for membership queries
+  #TMQ = 3 (ms)                      // time for membership queries
-  #TEQ = 48 (ms)                     // time for equivalence queries
+  #TEQ = 34 (ms)                     // time for equivalence queries
-  #TLEQ = 48 (ms)                    // time for the last equivalence query
+  #TLEQ = 34 (ms)                    // time for the last equivalence query
   #TTR = 0 (ms)                      // time for the translator
-  #TLR = 24 (ms)                     // time for the learner
+  #TLR = 16 (ms)                     // time for the learner
-  #TLRL = 7 (ms)                     // time for the learning leading automaton
+  #TLRL = 5 (ms)                     // time for the learning leading automaton
-  #TLRP = 7 (ms)                     // time for the learning progress automata
+  #TLRP = 5 (ms)                     // time for the learning progress automata
-  #TTO = 332 (ms)                    // total time for learning Buchi automata
+  #TTO = 147 (ms)                    // total time for learning Buchi automata
 </code>