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:41] – liyong | complement [2018/11/13 13:39] (current) – liyong | ||
---|---|---|---|
Line 1: | Line 1: | ||
====== Complementation ====== | ====== 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> | <code java> | ||
HOA: v1 | HOA: v1 | ||
Line 17: | Line 19: | ||
[0] 1 | [0] 1 | ||
--END-- | --END-- | ||
+ | </ | ||
+ | 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. | ||
+ | < | ||
+ | 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. | ||
+ | < | ||
+ | 2018/11/12 14:46:35 [ info] ROLL for BA complementation... | ||
+ | HOA: v1 | ||
+ | tool: " | ||
+ | properties: explicit-labels state-acc trans-labels | ||
+ | States: 2 | ||
+ | Start: 0 | ||
+ | acc-name: Buchi | ||
+ | Acceptance: 1 Inf(0) | ||
+ | AP: 1 " | ||
+ | --BODY-- | ||
+ | State: 0 | ||
+ | [(!0)] | ||
+ | [(0)] 0 | ||
+ | [(0)] 1 | ||
+ | State: 1 {0} | ||
+ | [(0)] 1 | ||
+ | --END-- | ||
+ | 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-- | ||
+ | #LT = 2 // #number of letters | ||
+ | #T.S = 2 // #states of target | ||
+ | #T.T = 4 // # | ||
+ | #H.S = 4 // #states of learned automaton | ||
+ | #H.T = 14 // # | ||
+ | #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 // # | ||
+ | #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 | ||
</ | </ | ||
complement.1542004871.txt.gz · Last modified: 2018/11/12 14:41 by liyong