====== Büchi Automata Complementation (Buechic) ======


Buechic is a tool to learn the complement of a given Büchi automaton. It is based on the learning library [[http://iscasmc.ios.ac.cn/roll/|ROLL]] [2]. We have added the support for [[http://adl.github.io/hoaf/|HOA]] format in ROLL. 

Buechic complements a given Büchi automaton B by learning an FDFA [1] which captures all ultimately periodic words of the complement of B. Therefore, our algorithm relies on the language of B instead of on the structure of B, as happens for the classic complementation techniques.

===== Source Code and Executable Files =====

  * {{ :buechic.zip |Buechic source code}} : the source code is released under [[https://www.gnu.org/licenses/gpl-3.0.en.html|GPL]] license
  * {{:buechic-jar.zip |Buechic executable file}}: Buechic jar file to complement Büchi automaton
  * {{ :buechi-universality.zip | Buechi complementation with Universality check}} : the jar file to complement Büchi automaton with universality checking

===== How to Use Buechic in Command Line =====
Buechic can be started using java -jar buechic.jar, which is equal to the following command.

<code>
java -jar buechic.jar -h
</code>

==== Running Buechic ====

The command to run Buechic to learn the Büchi automaton given by aut.hoa is:
<code>
java -jar buechic.jar aut.hoa -table -periodic
</code>

==== Data Structures ====

In Buechic,  you can specify the data structures for the learning procedure in the following.

  *  -table. This argument calls for the use of the observation table.
  *  -tree. It requires to use the classification tree for the learner.

==== Learning Algorithms ====

You can also use three canonical FDFAs to learn the Büchi automata as follows.

  * -periodic. Learning the periodic FDFA.
  * -syntactic. Learning the syntactic FDFA.
  * -recurrent. Learning the recurrent FDFA.


=== Lazy Equivalence Check ===

If you want to reuse the counterexample returned by the teacher as much as possible, you can use the
lazy equivalence check optimization as follows.
<code>
java -jar buechic.jar aut.hoa  -table -periodic -lazyeq
</code>

===== How to Use Buechic in JAVA Code =====

We support HOA format in Buechic. An example Büchi automaton is given as follows. 

=== Prepare a HOA file ===
<code java>
HOA: v1
name: "GFa"
States: 2
Start: 0
Start: 1
acc-name: Buchi
Acceptance: 1 Inf(0)
AP: 1 "a"
--BODY--
State: [0] 0 {0}
  0 1
State: [!0] 1
  0 1
--END--
</code>

=== Use the complement teacher ===
If you want to use Buechic in verification or other areas, you should use our complement teacher as follows.
<code java>
// initialize a parser to parse input automaton
Parser parser = new HOAParser(autfile);
FiniteAutomaton aut = parser.parse();

// prepare the data structure for alphabet
ValueManager contextValue = new ValueManager();
WordManager contextWord = new WordManager(contextValue);

// get an instance of our complement teacher
ComplementTeacherFDFA teacher = new ComplementTeacherFDFA(contextWord, aut);
</code>

=== Call a learner and specify the BA construction ===
<code java>
// specify FDFA learner, here we use table-based periodic FDFA learner
LearnerFDFA learner = new LearnerFDFATablePeriodic(contextWord, teacher);

// specify the counterexample translator
Translator ceTranslator = new TranslatorFDFAUnder(learner);
</code>

=== Learning loop ===
<code java>
System.out.println("Start learning...");
Timer timer = new Timer();
timer.start();
learner.startLearning();
timer.stop();
Statistics.timeLearner += timer.getTimeElapsed();
boolean result = false;
while(! result ) {
	
        Query<EqResult>	query = teacher.answerEquivalenceQuery(learner);

	// get out of the loop
	if(query.getQueryAnswer().isEqual == true) {
		Statistics.setLearnerFDFA(learner);
		Statistics.hypothesis = hypothesis;
		break;
	}
			
	// lazy equivalence check is implemented here
	ceTranslator.setQuery(query);
	while(ceTranslator.canRefine()) {
		Query<Boolean> ceQuery = ceTranslator.translate();
		timer.start();
		learner.refineHypothesis(ceQuery);
		timer.stop();
		Statistics.timeLearner += timer.getTimeElapsed();
                // set lazyEqCheck to true if you want to reuse the counterexample
		if(! lazyEqCheck) break;
	}

}
System.out.println("Learning completed...");		
</code>
----

===== Log Files =====
We have compared Buechic with [[http://goal.im.ntu.edu.tw/wiki/doku.php|GOAL]] on the automata from
[[http://buchi.im.ntu.edu.tw/|BüchiStore]] and [[https://github.com/xblahoud/NCSB-Complementation|NCSB-complementation]]. In the following, you can download the logs files of the experiments.
 
1. The Büchi Automata from BüchiStore can be found on their webpage and the log files are listed as below.

  * {{:buechic-buchistore-single.zip | single complementation on BüchiStore of Buechic }}
  * {{ :goal-buchistore-single.zip | single complementation on BüchiStore of GOAL}}
  * {{ :buechic-buchistore-double.zip | double complementation on BüchiStore of Buechic}}
  * double complementation on BüchiStore of GOAL:      
     * {{ :goal-piterman-double.zip |Piterman}}
     * {{ :goal-ramsey-double.zip |Ramsey}}
     * {{ :goal-rank-double.zip |Rank}}
     * {{ :goal-slice-double.zip |Slice}}
2. The Büchi Automata from NCSB-complementation and the log files are listed as below.
  * {{ :ncsb-automata.zip |NCSB automata in HOA format}} 
  * {{ :buechic-ncsb.zip |single complementation on NCSB-complementation of Buechic}}
  * single complementation on NCSB-complementation of GOAL: 
     * {{ :goal-ncsb.zip |NCSB}}
     * {{ :goal-piterman.zip |Piterman}}
     * {{ :goal-ramsey.zip |Ramsey}}
     * {{ :goal-rank.zip |Rank}}
     * {{ :goal-slice.zip |Slice}}


----

[1] Dana Angluin, and Dana Fisman. "Learning regular omega languages." In ALT. Springer International Publishing, 2014: 125-139.

[2] Yong Li, Yu-Fang Chen, Lijun Zhang, and Depeng Liu. "A Novel Learning Algorithm for Büchi Automata based on Family of DFAs and Classification Trees." In TACAS. Springer Berlin Heidelberg, 2017: 208-226.