complement
Differences
This shows you the differences between two versions of the page.
Both sides previous revisionPrevious revisionNext revision | Previous revision | ||
complement [2018/11/12 14:45] – liyong | complement [2018/11/13 13:39] (current) – liyong | ||
---|---|---|---|
Line 20: | Line 20: | ||
--END-- | --END-- | ||
</ | </ | ||
- | This Büchi automaton is the smallest automaton | + | This Büchi automaton is the smallest automaton |
- | + | ||
+ | As an example, one can use following command line to complement the given automaton. | ||
+ | < | ||
+ | java -jar ROLL.jar complement A.hoa -table -syntactic | ||
+ | </ | ||
+ | It will give us a complement automaton described in the Hanoi format as follows. | ||
+ | <code java> | ||
+ | HOA: v1 | ||
+ | tool: " | ||
+ | properties: explicit-labels state-acc trans-labels | ||
+ | States: 4 | ||
+ | Start: 0 | ||
+ | acc-name: Buchi | ||
+ | Acceptance: 1 Inf(0) | ||
+ | AP: 1 " | ||
+ | --BODY-- | ||
+ | State: 0 | ||
+ | [(!0)] | ||
+ | [(!0)] | ||
+ | [(!0)] | ||
+ | [(0)] 0 | ||
+ | [(0)] 3 | ||
+ | State: 1 | ||
+ | [(!0)] | ||
+ | [(!0)] | ||
+ | [(0)] 1 | ||
+ | [(0)] 2 | ||
+ | State: 2 {0} | ||
+ | [(!0)] | ||
+ | [(0)] 3 | ||
+ | State: 3 | ||
+ | [(!0)] | ||
+ | [(!0)] | ||
+ | [(0)] 3 | ||
+ | --END-- | ||
+ | </ | ||
The complete log information is the following. | The complete log information is the following. | ||
< | < | ||
- | 2018/11/12 14:41:08 [ info] ROLL for BA complementation... | + | 2018/11/12 14:46:35 [ info] ROLL for BA complementation... |
HOA: v1 | HOA: v1 | ||
tool: " | tool: " | ||
Line 79: | Line 115: | ||
#MQ = 4 // #membership query | #MQ = 4 // #membership query | ||
#EQ = 1 // # | #EQ = 1 // # | ||
- | #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 | #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 |
</ | </ | ||
complement.1542005144.txt.gz · Last modified: 2018/11/12 14:45 by liyong