Note: GOAL was made publicly available on 2006-08-23. There have since been several new releases, each introducing some changes and new features. Changes by earlier versions are not documented.

Next Release

[CORE] Draw alternating states correctly in the tikz outputs.
[CORE] Remove unreachable states when removing dead states.
[CORE] Fix a bug in detecting changed preferences.

2020-05-06

CORE: Run with JDK 11. Earlier versions of Java are no longer supported. Some Mac trackpad gestures do not work.
CORE: Add a conversion from NBW to SDBW.
CORE: Improve the search of automata conversions.
CORE, GUI: Add an option to disable overlaps of transition labels.
CORE: Disable overlaps of transition labels in HOAF outputs.
CORE: Fix a bug of inconsistent state comparison. Known affected algorithms: some operations on the results of Safra-Piterman determinization using history trees.
CORE: Fix a bug in PLTL2BA which generates unnecessary transitions to the sink.
CORE: Fix a bug in random generation of automata with acceptance on transitions.
CORE: Mark transition reduction in the conversion from NPW to NBW and parity simplification through the computation of Rabin index mutually exclusive. The two options are not compatible.
CORE: Fix a bug in ElementaryCycleGenerator. When using the elementary cycle generator to find cycles in a restricted area of an automaton, if the area is specified as clones of states of the automaton, then cycles won't be found.
CORE, CMD, GUI: Add an option to parse a single letter as a symbol for regular expressions and omega regular expressions.
CORE, CMD, GUI: Add determinization to WDBW formed by subset construction [DEK07].
CMD: Fix a bug in invoking classic complementation in command-line mode.
CMD: Fix a bug in deterministic command which always returns whether the input is semi-deterministic when checking whether the input is semantically deterministic.
CMD: Add arguments to output counterexamples for the emptiness command.
CMD: Fix a bug in the translate command where -se is treated as -sa.
CMD: Add a closure command.
GUI: Paste states with offsets to prevent overlapping.
GUI: Support editing Hanoi acceptance condition (experimental).

2015-10-18

CORE, GUI, CMD: Add subset construction (the acceptance condition of the output automaton is always empty).
CORE: Simplify the class Editable.
CORE: Re-implement the rank-based construction. The previous implementation has the following bugs.
- When tight rank is not enabled, not all possible level rankings are generated.
- The condition rank(f) = rank(f') in [Sch09] is not correctly implemented.
CORE: Add an implementation of the complementation construction based on progress measures [Kla91].
CORE: Add a complementation construction for Buchi automata in a two-layer hierarchical form.
CORE: Allow the extension of available generators in the generate command. Please note that some arguments of the random FSA and game generator have been changed.
CORE: Improve the conversion of alphabet types.
CORE: Add the support for Hanoi Omega-Automata (HOA) format.
CORE: Add a generator of semi-deterministic Buchi automata (SDBW).
CORE: Add a complementation construction for SDBW.
CORE: Fix a bug in the conversion from an NABW in DNF to an equivalent NBW. The result for an NABW with multiple (disjunctive) initial states is incorrect.
CORE: Improve the efficiency in transition simplification for large automata.
CORE: Add a codec that saves automaton structures only.
CORE: Improve the efficiency in reading large automata.
CORE: Add unambiguity test for NBW.
CMD, GUI: Add an action to test if an NBW is semi-deterministic.
CMD: Make the generate command extensible.
CMD: Change the class names XXXInterface to XXXExtension in the command-line package. Some method names in CommandRepository are also changed. Plugins that provide complementation constructions or game solvers for the command-line package have to be modified accordingly.
CMD: Improve goal.bat and add gc.bat for Windows.
CMD: Use a wiki-style format to write command-line help messages.
CMD: Preserve the order of arguments that contains –option.
GUI: Fix a bug in copying and pasting states.
GUI: Fix the status display of some menu items in the View menu.
GUI: Allow the extension of random automata generators.
GUI: Add an option to automatically remove unused atomic propositions from the alphabet when a state or a transition is deleted.

2014-11-17

CORE: Fix a bug in LBTTCodec which may accept ill-formed formulas.
CORE: Avoid the error message ”[Fatal Error] :1:1: Content is not allowed in prolog.” caused by parsing invalid XML documents by XML codecs.
CORE: Support the import of Promela never claim generated by Spin since version 6.2.4.
CORE: Fix a bug where the options for the Safra-Piterman construction are not passed to the conversion from NPW to NBW. Affected options: merge equivalent state, reduce transitions, and reduce states.
CORE: Fix a bug where the option of reducing transitions in Safra-Piterman construction is never applied.
CMD: Remove the past command. Use “qptl -p” instead.
CMD: Redesign the extensions available in the command-line package.
- CommandExpression and CommandExtension are redesigned.
- Allow direct extension of CommandExpression without CommandExtension.
- Extension of complementation constructions is redesigned. See the API documentation of ComplementExpression for more details.
- GameSolverInterface is redesigned.
CMD: Allow runtime arguments (specified by --option), that is, argument names and values determined at runtime. See the help page for more details.
CMD: Allow shell variables in the invocation of shell commands.
CMD: Add an import command.
CMD: Allow lists in GOAL scripts. Indices are returned when iterating over an array while list items are returned when iterating over a list.
GUI: Change the hotkey of complementation to Ctrl-Alt-C.
GUI: Fix a bug where the height of the message panel may grow during step-by-step complementation.

2014-08-08

CORE: Implement Schewe's history trees for the determinization of Buechi automata.
CORE: Enhance the dot codec.
CORE: Add an implementation of automata-based string replacement.
CORE: Allow exporting multiple objects to a single file.
CORE: Add a conversion from NSW to NGBW.
GUI: Allow arrows as initial indicators.
GUI: Allow copying and pasting states.
CMD: Make the solve command keep the annotations of winning regions and winning strategies on the input game.
CMD: Make the alphabet command always return the new alphabet of the input automaton. The alphabet manipulation is directly applied to the input automaton.
CMD: Provide hints when the user provides a wrong command name.

2013-07-11

CORE: Remove an unnecessary import of a class from Sun such that GOAL can be executed with OpenJDK.
CORE: Improve the pattern matching of QPTL formulae.
CORE: Add an implementation of the separation of past and future operators [Gab87].
CORE: Slightly improve the conversion of label positions.
CORE: Add a conversion from a deterministic automaton to a turn-based game.
CORE: Add a preference for adjusting the default alphabet type and the default label position of new automata and games.
CORE: Add alphabet abstraction, which can replace existing atomic propositions by predicates.
CORE: Make some game solvers able to be performed step-by-step.
CORE: Allow saving automata with transition labels simplified.
CORE: Fix a bug in generating unique QPTL formulae.
CORE: Fix a bug that overwrites the name of an automaton by its description in the saved GFF file.
CORE: Fix a bug in the computation of attractors when there are dead ends. This bug may make the Recursive solver produce incorrect results when the input game has dead ends.
CORE: Fix a bug in LTL2BUCHI.
GUI: Cache images files of Buechi Store locally.
CMD: Add a command for manipulating alphabets.
OTHER: Improve the startup script for Windows. If java.exe is not in the search path, the script will try to find it in some predefined paths.
OTHER: Add two scripts that can generate library files (JAR) from the three GOAL plugins. The generated files can be imported when developing applications that use functions of GOAL.

2013-01-23

CORE: Add a function for compressing parity conditions.
CORE: Add a function for propagating parities of states in a parity condition.
CORE: Add an implementation of the big step solver for parity games due to Sven Schewe.
CORE: Add a parity game solver which can apply solver-independent global optimizations to the input parity game before delegating the game solving to another parity game solver.
CORE: Make the description of the implementation of small progress measure more precise: the optimizations described in the original paper are not included in the implementation.
CORE: Make the GameSolver interface able to solve a subgame.
CORE: Implement DFS and double DFS by stacks.
CORE: Implement the computation of the fair simulation relation for an NBW based on [EWS01] and [GBS02].
CORE: Add simplification with fair simulation for NBW (both label-on-states and label-on-transitions).
CORE: Implement the computation of the delayed simulation relation for an NBW based on [EWS01].
CORE: Add simplification with delayed simulation for NBW (both label-on-states and label-on-transitions).
CORE: Make Naive Simulation support finite state automata with acceptance on transitions.
CORE: Make simplification with direct and reverse simulation relations support finite state automata with acceptance on transitions.
CORE: Make the postponed expansion of refined states an option for the extended on-the-fly translation algorithms.
CORE: Add an advanced reduction of NTGBW transitions during the conversion from two-way VWAA.
CORE: Improve the parsing of QPTL quantifications.
CORE: Slightly improve the Promela codec.
CORE: Make the convert command support the conversion of alphabet types.
CORE: Use prime implicants to simplify Boolean expressions in Couvreur's algorithm.
CORE: Do not remove dead states after converting the label position of an automaton.
CORE: Extend MoDeLLa for past operators.
CORE: Extend LTL2Buchi for past operators.
CORE: Extend Couvreur's algorithm for past operators.
CORE: Add an option to use prime implicants to simplify covers for LTL2AUT+.
CORE: Add an implementation of the translation algorithm in [CCJ09] which can obtain minimal Buechi automata for certain classes of LTL formulae.
CORE: Add a generator that can generate a complete set of finite state automata of a specified state size and a specified alphabet size.
CORE: Add an implementation of the cycle finding procedure in [Joh75].
CORE: Add an implementation of testing if a language, a classic finite automaton, or a Buechi automaton is aperiodic (star-free, counter-free) based on [DG08].
CORE: Add two options to Tableau to keep unreachable and dead states of the label-on-state NGBW.
CORE: Add a codec for the formats of generalized Buechi automata and LTL formulae used in LBTT.
CORE: Add a function for taking products. The acceptance condition of a product only depends on one of the inputs.
CORE: Fix a bug in decoding files output by MoDeLLa which does not set the alphabet.
CORE: Fix a bug in decoding files output by LTL2Buchi which does not set the alphabet.
CORE: Fix a bug in converting an alternating Buchi automaton in CNF with an empty alphabet to an equivalent Buchi automaton.
CORE: Fix a bug in classifying an empty automaton into the Temporal Hierarchy.
CORE: Fix a bug which incorrectly translates some LTL formulae such as ”((~) ~ p) R (-) p” by PLTL2TWVWAA.
CORE: Fix a bug in random formulae generation where the option “must contain at lease one past operator” is not working.
CORE: Fix a bug in translating QPTL formulae with a sub-formula inside a universal quantification.
CORE: Fix a bug in reducing dead states for alternating automata. This bug may make LTL2BA produce incorrect results for formulae such as ()([](p /\ ~p) /\ q).
CORE: Fix a bug in simultaneous literal renaming with conflicts.
CORE: Fix a bug in determining if an automaton is semantically deterministic. This bug makes the procedure incorrectly report that an automaton is semantically deterministic in some cases.
CORE: Fix a bug in the representation of two-way alternating automata. Previously, transitions from the same source state to the same destination state with the same label but in different directions are not allowed. This bug may make PLTL2BA produce incorrect results.
CORE: Fix a bug in Modella that does not follow the original paper to impose fairness conditions.
GUI: Make the positions in the acceptance condition a property of states and transitions such that the positions can be displayed on states and transitions.
GUI: Remove the requirement of initial states from the game solving action.
GUI: Add menu items for testing if one automaton is direct simulated, delayed simulated, or fairly simulated by another automaton.
GUI: Add an option to display gridlines as dots.
GUI: Allow the rotation of automata with Mac trackpad.
GUI: Add a search field to the repository dialogs.
GUI: Enable equivalence testing between a label-on-state automaton and a label-on-transition automaton.
GUI: Parse words smarter.
GUI: Add a new interface for editing input words.
GUI: Make the Buechi Store browser able to display automata of various types.
GUI: Add an interactive input simulator.
GUI: Fix a bug that totally ignores the transparency option when drawing gridlines.
GUI: Fix a bug in creating folders in a file saving/opening dialog.
GUI: Fix a bug in viewing run trees and run DAGs for classic finite automata. Due to this bug, finite words are not accepted.
GUI: Fix the wrong classification of temporal hierarchy and spec patterns in the Buechi Store browser caused by the change of Buechi Store database.
CMD: Allow +=, -=, *=, /=, %=, &=, |=, ++, and – in the command-line mode.
CMD: Do not convert null to 0 when used as integers and the operation is equality or inequality. Otherwise, $x == null may be true if $x is 0.
CMD: Make the echo command able to output a QPTL formula in the SPIN format. Note that associativity and precedence of operators in GOAL are different from those in SPIN.
CMD: Make the simplify command able to simplify logic formulae.
CMD: The working directory is no longer changed in the startup shell scripts.
CMD: Add a startup shell script “gc” that does not load any Java GUI components. If you don't need any graphical interface, use “gc” rather than “goal” to invoke GOAL.

2012-04-09

CORE: Fix a bug in the slice-based complementation that does not create the transition relation cache correctly when the option of total transition relation is on.
CORE: Fix a bug in parsing quantified formulae.
CORE: Fix a bug that makes the conversion of QPTL formulae to prenex normal form not working.
CORE: Fix a bug in comparing objects of State and objects of sub-classes of State. The conversion to NMW from an NBW obtained by Safra-Piterman complementation may produce incorrect automata due to this bug.
CORE: Fix a bug in the test if an automaton is semantically deterministic, which does not check all cycles.
CORE: Fix a bug in computing the state symbol simulation.
CORE: Fix a bug in isomorphism and homomorphism which may not find the mapping in some cases.
CORE: Fix a bug in reducing unreachable and dead states of an NMW. In this bug, when an unreachable or dead state is removed, it is also removed from the acceptance condition. As a result, the language of the NMW may be changed.
CORE: Fix a bug in encoding and decoding transition co-Buchi acceptance condition.
CORE: Fix a bug in determining if two states have the same alpha successors for alternating automata.
CORE: Fix a bug in expanding the alphabet of a two-way alternating automaton. This bug may change the backward transitions to forward transitions.
CORE: Fix a bug in applying simulation simplification to automata with empty alphabet.
CORE: Fix a bug that does not save the final states of two-way alternating automata to GFF.
CORE: Fix a bug in equivalence checking that does not accept as inputs alternating automata convertible to equivalent NBW.
CORE: Fix a bug in applying Theorem 5 of pruning fair sets to label-on-state automata.
CORE: Add a simple boolean expression simplification to the Couvreur's translation algorithm.
CORE: Add a conversion from NBW to NCW by the approach in [BK09]. The NCW is equivalent to the NBW if the NBW is NCW-recognizable. Otherwise, the NCW will contain the NBW.
CORE: Add a conversion from NBW to equivalent DBW (if possible) through DCW by the approach in [BK09].
CORE: Add the classification of temporal formulae and automata into the temporal hierarchy.
CORE: Add a conversion from NCW to NMW.
CORE: Allow V for the release operator.
CORE: Add a translation algorithm from a QPTL formula without past operators to an equivalent NBW. The QPTL formula is not required to be convertible to prenex normal form.
CORE: Add options for simplification with simulation.
CORE: Add a translation from an ACTL formula to a fair Kripke structure by a modified construction based on [PMT02]. Currently, the Kripke structure is represented by an automaton in GOAL. Further operations on the automaton may change the relation between the ACTL formula and the Kripke structure.
CORE: Add two QPTL rewrite patterns.
CORE: Add the support of reversing classic finite state automata.
CORE: Add an option to the conversion from NTGBW to NBW by LTL2BA for reducing dead states before merging equivalent NBW states.
CORE: Make the removal of dead states really remove dead states for omega automata that are not NBW. Previously, the implementation keeps a state if it can visit some accepting state (a state in the acceptance condition) infinitely often. This does not guarantee that the state will be in some accepting run for omega automata that are not NBW.
CORE: Add a codec that can encode an automaton in the GasTeX format.
CORE: Add a codec that can encode an automaton in the Tikz format.
CORE: Add a codec that can encode an automaton in the Vaucanson-G format.
CORE: Add a translation from QPTL formulae in canonical forms to an equivalent NBW. Formulae that have boolean operators, future operators, or quantifications applied outside sub-formulae in canonical forms are also supported.
CORE: Add the classification of QPTL formulae into the standard kappa-formulae [CMP92].
CORE: Add a random game generator.
CORE: Make the QPTL parser support && and ||.
CORE: Add support of the trigger operator to Tableau, Incremental Tableau, Temporal Tester, and extended on-the-fly translations.
CORE: Add more transformation for converting a QPTL formula into prenex normal form.
CORE: Add a codec for PGSolver.
CORE: Create a superclass for alternating automata and two-way alternating automata.
CORE: Add an implementation of the translation from full QPTL formulae to Buchi automata in KP02.
CORE: Add four parity game solvers: Recursive, McNaughton-Zielonka, Dominion Decomposition, and Small Progress Measure.
CORE: Add a reachability game solver.
CORE: Add a classical Buchi game solver.
CORE: Add some conversions between games.
CORE: Add conversions between parity interpretations, including min-even, min-odd, max-even, and max-odd.
CORE: Make the user able to choose the dual operators of until and since.
GUI: Fix a bug in the conversion to NMW which does not display the options dialog when the source automaton is deterministic.
GUI: Fix a bug in editing classic and co-Buchi acceptance conditions by double clicking.
GUI: Fix a bug that displays transition labels even if None is selected in the transition attributes of the automaton popup menu.
GUI: Fix a bug that displays the name of an alternating connector.
GUI: Remove duplicate fields in the property editors for automata and alternating automata.
GUI: Disable the conversion of alternating style for two-way alternating automata.
GUI: Add a menu item for merging two automata.
GUI: Add the options panel for pruning fair sets to the preference dialog.
GUI: Open the help page on the client's default browser for non-Mac users because the built-in Java browser does not support XHTML internal entities.
GUI: Add an editor for transition co-Buchi acceptance condition.
GUI: Disable the transition label editing for alternating transitions from connectors to states.
GUI: Display more state properties when the mouse cursor is idling on a state.
GUI: Enforce the validity of parity conditions in GUI.
GUI: Add options for the outputting formats of QPTL formulae.
GUI: Add actions for converting a logic formula into negation normal form or prenex normal form if it is possible.
GUI: If a codec is selected in the open file dialog, use the codec to decode the file.
CMD: Fix a bug in the repository command which requires the return type in capital letters.
CMD: Fix a bug in comparing objects of different types.
CMD: Fix a bug in evaluating the Boolean condition of a while statement.
CMD: Remove duplicate formulae returned by the command “repository -t formula remote”.
CMD: Add an option to the repository command for retrieving only the smallest automata.
CMD: Add a try/catch statement.
CMD: Reuse windows in command-line mode to prevent memory leaks.
CMD: Allow wildcards in shell commands.
CMD: Add an option to the close command such that a window can be closed without displaying any dialog for saving objects.
CMD: Allow the concatenation command to concatenate strings.
CMD: Add the missing classic complementation back.
CMD: Set default complementation constructions for the complement command.
CMD: Make the reduce command operate on a clone of the input automaton.
CMD: Add an implicit conversion from a string variable to an array in the command-line mode.
CMD: Open options for pruning fair sets in the command-line mode.

2011-10-10

CORE: Open more options of KK layout.
CORE: Add a naive tree layout.
CORE: Add an on-the-fly containment test with the Safra's construction.
CORE: Add an on-the-fly containment test with the Muller-Schupp construction.
CORE: Add an on-the-fly containment test with the Safra-Piterman construction.
CORE: Add an on-the-fly containment test with the slice-based construction.
CORE: Add a codec to support the BA format in http://www.iis.sinica.edu.tw/FMLAB/CAV2010.
CORE: Add the simplification of Buchi acceptance set.
CORE: Add implementations of the SchematicSimilarity1 procedure, the RefinedSimilarity procedure, and the EfficientSimilarity procedure in [HHK95].
CORE: Add a conversion from label-on-transition FSA to label-on-state FSA.
CORE: Add support of regular expressions and omega regular expressions.
CORE: Add a codec for encoding/decoding NFW in/from JFLAP file format.
CORE: Add conversions from NBW to NTBW, from NTBW to NTGBW, and from DNFNABW to NBW.
CORE: Implement the heuristic of “all successors are accepting” in [KB06].
CORE: Make the QPTL unification able to unify two QPTL formulae that are equal up to literal renaming.
CORE: Re-implement the Muller-Schupp construction.
CORE: Re-implement the determinization of NFW. The original implementation will not work if the states of the input NFW do not have consecutive IDs starting from 0.
CORE: Improve the implementation of the Ramsey-based complementation.
CORE: Add an option for the Ramsey-based construction to minimize the intermediate DFW.
CORE: Add a codec for exporting automata as SVG files.
CORE: Allow && and || in QPTL formulae.
CORE: Return true and the input automaton respectively in the semantically deterministic test and in the conversion to DBW if the input automaton is already a DBW.
CORE: Add a function for performing omega operation on an NFW.
CORE: Add an implementation of the Hopcroft's DFW minimization algorithm.
CORE: Add a function for the concatenation of an NFW and an omega automaton.
CORE: Support epsilon-transitions of an NFW with a classical alphabet.
CORE: Add testing of homomorphism and isomorphism.
CORE: Add conversion of alternation styles (DNF/CNF).
CORE: Re-implement the Couvreur's translation algorithm. The previous implementation in GOAL1 does not merge equivalent states.
CORE: Re-implement the translation from LTL to VWAA in LTL2BA.
CORE: Re-implement the conversion from VWAA to NTGBW in LTL2BA. The previous implementation in GOAL1 does not handle the empty conjunction, and thus many more states are created.
CORE: Re-implement the conversion from NTGBW to NBW in LTL2BA.
CORE: Re-implement LTL2BUCHI.
CORE: Re-implement PLTL2BA. Compared with the previous implementation in GOAL1, this implementation produces fewer states but takes longer time.
CORE: Add a direct conversion from NTGBW to NGBW.
CORE: Add a conversion from DMW to complement DMW.
CORE: Add conversions from DMW to equivalent DRW, equivalent DSW, and equivalent DPW.
CORE: Add a conversion from NBW to complement UCW and a conversion from NCW to complement UBW.
CORE: Add a conversion from DBW to complement DCW and a conversion from DCW to complement DBW.
CORE: Add a conversion from NCW to equivalent DCW.
CORE: Add a conversion from DCW to equivalent NBW.
CORE: Do nothing in reducing dead states for alternating automata.
CORE: Make the property names in the GFF files case sensitive.
CORE: Fix a bug in making the transition display complete which will remove custom transition properties.
CORE: Fix a bug in proposition projection which may delete transitions.
CORE: Fix a bug in classical symbol projection which may introduce ε transitions.
CORE: Fix a bug in opening a GFF file which does not sort the propositions.
CORE: Fix a concurrency bug in the conversion from NPW to NBW. The results may be incorrect if more than one CPU core is allocated.
CORE: Fix a bug in converting NRW to NBW.
CORE: Fix a bug in reducing dead states of an NFW.
CORE: Fix a bug in pruning fair sets that does not compute the fair SCCs correctly.
CORE: Fix a bug in applying theorem 7 in pruning fair sets.
CORE: Fix a bug in NFW union which does not make the initial state of the union accepting when some initial state of the input NFW is accepting.
CORE: Fix a bug in the checking of syntactical determinism.
CORE: Fix a bug in the NFW containment which does not equalize the alphabet before complement.
CORE: Fix a bug in the conversion from NGBW to NBW that does not set the transition display correctly, which may make other operations produce incorrect results.
CORE: Fix a bug in the random FSA generator which does not set the transition-based acceptance conditions correctly if acceptance density is used.
CORE: Fix a bug in literal comparison.
CORE: Fix a bug in the GPVW translation where the option of NBW simplification is not applied.
CORE: Fix a bug in the MoDeLLa translation where the option of formula simplification is not applied.
CORE: Fix a bug in computing pre-image and post-image of a state set, which makes the pruning fair sets produce wrong results.
CORE: Fix a bug in the complementation via weak alternating automaton that does not create transitions from the sink state to itself correctly.
CORE: Fix a bug in input testing that does not work correctly on NMW.
CORE: Fix a bug in random LTL formulae generation that always extends the number of propositions by the same proposition.
CORE: Fix a bug in the Landweber's conversion from DMW to DBW where the equality of DBW states are decided incorrectly.
GUI: Add more guidelines.
GUI: Add an option for displaying gridlines.
GUI: Add color and opacity fields to the property editors of states and transitions.
GUI: Add an option to the search dialog for exact match.
GUI: Add an uploader of the Buchi Store.
GUI: Add a coloring tool.
GUI: Add new icons.
GUI: Add the visualization of Safra trees, Muller-Schupp trees, and compact Safra trees.
GUI: Add import from text.
GUI: Add layout animation.
GUI: Add the visualization of run trees, run DAGs, split trees, and reduced split trees.
GUI: Add automaton ID and formula ID in the Buchi Store viewer.
GUI: Allow the user to insert user-defined properties to editable objects in the property editor.
GUI: Allow the user to display custom properties on states and transitions.
GUI: Validate parameters for creating a random FSA.
GUI: Preview logic formulae.
GUI: Make transitions searchable.
GUI: Simplify the transition display of the automata obtained from the Buchi Store for formula translation.
GUI: Display the Buchi Store dialog faster by loading automata in the background.
GUI: Hide the progress dialog when the containment test, equivalence test, or the semantically deterministic test is done.
GUI: Allow the user to create more than one transition from one state to another state by using ”,” to separate the symbols.
GUI: Allow deleting selected states and transitions by Backspace or Delete.
GUI: Create a default initial state automatically after creating a new automaton.
GUI: Refresh the acceptance condition editor when the acceptance condition is modified.
GUI: Add an action for custom automaton conversions.
GUI: Make labels of accepting transitions mergeable.
GUI: Improve the parity assignment in the acceptance condition dialog.
GUI: Fix a bug in the property editor where only one new property can be saved at a time.
GUI: Fix a bug which makes the function of snapping states to a grid fail sometimes.
GUI: Fix a bug that does not terminates the tool when closing the last window and then saving some object.
GUI: Fix a bug that does not display the QPTL property editor.
GUI: Fix a bug in the alternating automata property editor where the alternating style field is editable.
GUI: Fix a bug in undoing an alphabet contraction action which does not recover deleted transitions.
GUI: Fix a bug in undoing transition creation that introducing new propositions.
GUI: Fix a bug in tab DnD where the dropping target will not receive events from the dropped tab.
GUI: Fix a bug that cannot remove a state from the initial states of a label-on-state automaton.
GUI, CMD: Fix bugs in loading 3rd-party extensions.
CMD: Add an input test command.
CMD: Add a simulated command for testing if an automaton can be simulated by another automaton.
CMD: Change the result of a containment to a pair of a boolean and an object. The boolean indicates if the first automaton is contained in the second automaton. The object represents the counterexample found.
CMD: Add translation from QPTL to label-on-state NBW and label-on-state NGBW to the command-line mode.
CMD: Fix a bug that the command “deterministic” and the command “determinable” never perform determinism test.
CMD: Merge the “determinable” command and the “deterministic” command.

2011-02-14

Note: this is a preview version.

Redesign user interface:
- Tabbed window
- Startup dialog
- History of recently opened files
- A focus tool for concentrating on a state and its neighbors
- Select and drag multiple states
- Snap states to a grid
- Drag and drop to open files
- Preview an automaton in the file selection dialog
- Drag and drop tabs
- and many more
Redesign internal data structures and some algorithm implementations.
Make the tool extensible by plugins based on the Java Plugin Framework.
Redesign GFF (GOAL File Format).
Make automata and formulae generation functions accessible in the graphical user interface.
Make more functions directly applicable to omega automata other than NBW, for example generation function, conversion functions, input test, emptiness test, etc. The conversion to NBW is done automatically.
Make functions of finding MSCC, finding elementary cycles, and computing simulation relations accessible in the graphical user interface.
Implement the simplification of parity acceptance condition through the computation of the Rabin index.
Add a viewer of the Büchi Store.
Acceleration in some places with multi-cores.
Implement 7 layout creation algorithms:
- Circle Layout
- FR Layout
- GEM Layout
- ISOM Layout
- KK Layout
- Random Layout
- SA Layout
Implement 3 layout adjustment algorithms:
- Force-Scan Algorithm
- Force-Transfer Algorithm
- Improved Push Force-Scan Algorithm
Add the ability to import the never claims output by SPIN.
Add the checking for GOAL udpates.
Add support for Mac multi-touch trackpad:
- Switch windows
- Switch tabs
- Zoom in/out
Allow the renaming from a proposition to a literal.

2010-12-18

Fix a bug in the slice-based construction that merges some elements of an undecorated slice when the enhanced guess is applied.
Fix a bug in the slice-based construction where the configuration options have wrong dependency.
Add the Ramsey-based complementation.
Add the preliminary version of the slice-based construction.
Improve maximizing acceptance set by finding MSCCs instead of cycles.
Fix a bug in LTL2BA where a NullPointerException may be thrown sometimes in some cases.
Re-implement MoDeLLa with postponement, merging states, and pruning fair sets optimizations described in the original paper but never implemented in previous versions.
Fix a bug in translation options where the option of simplifying projected NBW has no effect.
Fix a bug in Couvreur such that formulae with []<> operators can be translated correctly.
Fix a bug in the conversion from TGBA to BA in LTL2Buchi.
Fix a bug in LTL2Buchi where a NullPointerException may be thrown sometimes in some cases.

2010-02-01

Fix a bug that rejects a transition labeled by lambda. This bug causes Safra's complementation failed to produce the correct result.
Add an option to apply divide and conquer translation.
Add an option to apply simplification to GBA (NGBW) before converting it into a BA (NBW).
Add the support of converting an NSW to an NMW.
Allow users to apply simplification at the intermediate steps of a QPTL formula translation.
Fix a bug in converting an NMW to an NBW.
Fix a bug that breaks the orderedness of states returned by getStates() after reordering states. This bug will make the algorithm converting an NSW to an NBW produce incorrect results if the states of the NSW are reordered before conversion.
Fix a bug that makes the algorithm converting an NSW to an NBW produce incorrect results if the IDs of the states of the NSW are not continuous and starting from 0.
Fix a bug in satisfiability checking where the reverse answer is given.
Add the support of conversion from Buchi automata to Promela code in command-line mode.
Add the support of slice-based complementation.
Add while-statement, seq command, reduce command, break instruction, and continue instruction to the command-line mode.
Allow the random automata generator to generate automata that cannot be reduced or simplified anymore.
Allow users to query the usage of a specific command in the command-line mode. For example, “java -jar goal_????_??_??.jar help complement” will only show the usage of the complement command.
Add a direct conversion from parity automata to Buchi automata. The previous conversion is performed by converting a parity automaton to a Rabin automaton and then to a Buchi automaton.
In random automata generator, use a double instead of an integer for the probability of creating a transition between two states.
Add a local optimization in the conversion from NPW to NBW.
Add more options to the random Buchi automata generator.
Fix a bug in extended on-the-fly translations that does not set the generalized Buchi acceptance condition correctly when there is no state that can satisfy a fair LTL formula.
Fix a bug that does not evaluate boolean expressions containing boolean operators in command-line mode.
Fix a bug that does not parse boolean constants correctly in the command-line mode.
Improve the performance of simulation simplification.
Add the support of rank-based complementation.
Add the support of simplification for formula.
Command-line arguments can be accessed by $0, $1, … in a GOAL script.
Add some optimizations to Safra-Piterman construction.
Allow MoDeLLa, Couvreur's algorithm, and LTL2BUCHI to support formulae with quantifications.
Fix a bug in Safra's construction that does not allocate enough Rabin acceptance pairs.
In Safra's construction, use creation time to determine older siblings instead of node name such that the implementation conforms to the construction of the paper.
In Safra-Piterman construction, assign n+1 (where n is the state size of the input NBW) to e and f if there is no node removed during tree transformation such that the implementation conforms to the construction of the paper.
Add a menu item for maximizing the Buchi acceptance condition.
Add a menu item for testing the temporal hierarchy of a QPTL formula.
Add a circle layout for automata with small state size.
Add a link to BuchiStore (http://buchi.im.ntu.edu.tw/).

2009-04-19

Fix a bug that does not read the preference of user-defined translation algorithm correctly.
Fix several bugs involving classical alphabet.
In Rename Proposition/Symbol and Contract Alphabet, only display available options.
Add an option in the preference for application of simplification after obtaining a NBW or a NGBW.
Add syntactical unification between two QPTL formulae. This will be useful if the option “Use the Repository for Formula Translation” is enabled.
Fix a bug that allows invalid propositions.
Add the conversion from alternating Büchi automata to Büchi automata back.
Temporarily disable the stage-by-stage complement via weak alternating automata.

2009-03-21

Add new translation algorithms from QPTL formulae to equivalent omega automata, including MoDeLLa (ST), On-the-fly (Couvreur), LTL2Büchi (GL), and LTL2VWAA (GO).
Add the support of classic finite automata. Several operations such as union, intersection, determinization, etc are also available.
Add determinization of Büchi automata. The result can be deterministic Rabin automata or deterministic Parity automata.
Add the test of on-the-fly model checking which performs on-the-fly intersection step-by-step.
Remove the conversion from alternating automata to Büchi automata temporarily because the conversion can only be applied to weak alternating automata.

2008-08-25

Added batch execution of commands in command-line mode.
Separated the translate command in command-line mode into translate (from formulae to automata) and convert (from automata to automata).
Separated the font setting into GUI font and drawing font. GUI font is used in GUI components such as menu items while drawing font is used in drawing omega automata or game graphs.

2008-06-21

Renamed and added some tags in GFF.
Added support for drawing alternating automata and games.
Added the implementation of Kurshan's complementation algorithm for DBW.
Added the implementation of Muller-Schupp complementation algorithm.
Added the stage-by-stage option to four more complementation algorithms:
- modified Safra's construction, Muller-Schupp construction,
- complement via very weak alternating parity automata, and
- complement via very weak alternating automata.
Added support for stage-by-stage complementation in the command-line mode.
Added support for duplicate without ACC.
Added support for changing the GUI font.

Table of Contents