usage
Differences
This shows you the differences between two versions of the page.
| Both sides previous revisionPrevious revisionNext revision | Previous revision | ||
| usage [2018/11/14 11:34] – [From an FDFA to a BA] liyong | usage [2018/11/15 20:21] (current) – [Lazy Equivalence Check] liyong | ||
|---|---|---|---|
| Line 12: | Line 12: | ||
| java -jar ROLL.jar command input_files [options] | java -jar ROLL.jar command input_files [options] | ||
| </ | </ | ||
| - | The available commands in ROLL are summarized as running modes in the following and the introduction of the options available in the tool is also provided | + | The available commands in ROLL are summarized as running modes in the following and the introduction of the options available in the tool is also provided. |
| ==== Running Modes ==== | ==== Running Modes ==== | ||
| Line 19: | Line 19: | ||
| * **help**. Show the help page (same as the option -h). | * **help**. Show the help page (same as the option -h). | ||
| - | * **test n k**. Test the learning algorithms implemented in the tool with n randomly generated Büchi automata of k states. This mode tries to detect | + | * **test n k**. Test the learning algorithms implemented in the tool with n randomly generated Büchi automata of k states. This mode tries to expose |
| * **play**. You play a teacher to teach ROLL to learn a language you have in mind. **An example can be found [[play|here]]**. | * **play**. You play a teacher to teach ROLL to learn a language you have in mind. **An example can be found [[play|here]]**. | ||
| * **learn < | * **learn < | ||
| Line 66: | Line 66: | ||
| ROLL supports both // | ROLL supports both // | ||
| - | * -table. Choose the observation tables (**default setting**). | + | * |
| - | * -tree. Use classification trees. | + | * |
| ==== Learning Algorithms for Büchi automata ==== | ==== Learning Algorithms for Büchi automata ==== | ||
| Line 73: | Line 73: | ||
| There are two learning algorithms for Büchi automata in ROLL, namely the L< | There are two learning algorithms for Büchi automata in ROLL, namely the L< | ||
| The default learning algorithm for Büchi automata in ROLL is the L< | The default learning algorithm for Büchi automata in ROLL is the L< | ||
| - | For the L< | + | For the L< |
| - | * -periodic. Learning based on the periodic FDFA. | + | |
| - | * -syntactic. Learning based on the syntactic FDFA (**default setting**). | + | |
| - | * -recurrent. Learning based on the recurrent FDFA. | + | |
| - | You can also use the option -ldollar instead to select the L< | + | You can also use the option |
| An example of the use of the L< | An example of the use of the L< | ||
| < | < | ||
| Line 90: | Line 90: | ||
| - | * -under. This method under-approximates the ultimately periodic words accepted by the conjectured FDFA. | + | |
| - | * -over. It over-approximates the ultimately periodic words accepted by the conjectured FDFA. | + | |
| === Limit Deterministic Büchi Automata === | === Limit Deterministic Büchi Automata === | ||
| - | You can also get a limit deterministic Büchi automaton as the final output automaton by giving the option -ldba when using the L< | + | You can also get a limit deterministic Büchi automaton as the final output automaton by giving the option |
| - | An example is given as below. | + | An example is given below. |
| < | < | ||
| java -jar ROLL.jar learn aut.ba -table -periodic -ldba | java -jar ROLL.jar learn aut.ba -table -periodic -ldba | ||
| Line 105: | Line 105: | ||
| If you want to reuse the counterexample returned by the teacher as much as possible, you can use the | 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 (NOT TESTED). | + | lazy equivalence check optimization as follows (NOT FULLY TESTED). |
| + | This option is **not encouraged** since it may result in larger output automaton. | ||
| < | < | ||
| java -jar ROLL.jar learn aut.ba -table -periodic -lazyeq | java -jar ROLL.jar learn aut.ba -table -periodic -lazyeq | ||
| Line 112: | Line 113: | ||
| ==== Counterexample Analysis ==== | ==== Counterexample Analysis ==== | ||
| - | When receiving a counterexample, | + | When receiving a counterexample, |
| - | By default, ROLL will use linear search to find that suffix, but you can also choose to use binary search to do that by giving the option **-bs** | + | By default, ROLL will use a linear search to find that suffix, but you can also choose to use binary search to do that by giving the option **-bs** |
| ==== Verbose Log Level ==== | ==== Verbose Log Level ==== | ||
| Line 119: | Line 120: | ||
| The argument **< | The argument **< | ||
| With the default verbose log level 0, there is a minimal output for the learning procedure. | With the default verbose log level 0, there is a minimal output for the learning procedure. | ||
| - | You can see a sequence of log messages like ``Analyzing counterexample for FDFA learner..." | + | You can see a sequence of log messages like ``Analyzing counterexample for FDFA learner..." |
| You can see more details on the learning procedure with the verbose log level 2, such as the current observation table of the learner. | You can see more details on the learning procedure with the verbose log level 2, such as the current observation table of the learner. | ||
| However, with the verbose log level 2, you may see some word which is a sequence of unprintable characters. | However, with the verbose log level 2, you may see some word which is a sequence of unprintable characters. | ||
| - | This is because we map every original input letter to an integer value as a character in our **Alphabet** object. Nonetheless, | + | This is because we map every original input letter to an integer value as a character in our **Alphabet** object. Nonetheless, |
| ===== Automata Format ===== | ===== Automata Format ===== | ||
usage.1542166452.txt.gz · Last modified: 2018/11/14 11:34 by liyong