| Version | Date | Description |
|---|
| 1.0.8 | 2008-05-21 | for jABC 3.6a |
| 1.0.7 | 2008-04-11 | for jABC 3.6 |
| 1.0.3 | 2007-12-13 | for jABC Release 3.5.1 |
| 1.0.1 | 2007-06-29 | for jABC Release 3.3 |
| 1.0.0-RC3 | 2007-01-23 | for jABC Release 3.0.7 |
| 1.0.0-RC2 | 2006-10-12 | for jABC Release 3.0 Beta 1 |
| 1.0.0-RC1 | 2006-09-12 | for jABC Release 3.0 alpha 4 |
| 0.9.9^n | 2006-06-21 | for jABC Release 2.5.0 |
| 0.9.05 | 2006-03-06 | for jABC Release 2.4.2 |
| 0.9.04 | 2006-02-13 | for jABC Release 2.4.2 |
| 0.9.03 | 2006-01-30 | for jABC Release 2.3.2 |
| 0.9.02 | 2006-01-26 | for jABC Release 2.3.2 |
| 0.9.01 | 2005-12-19 | for jABC Release 2.3.0 |
| 0.9.00 | 2005-10-31 | for jABC Release 2.1.1 |
| 0.8.13 | 2005-10-12 | for jABC Release 2.1.0 |
| 0.8.12 | 2005-09-21 | for jABC Release 2.0.1 |
| 0.8.08 | 2005-09-05 | for jABC Release 2.0.1 |
| 0.8.05 | 2005-08-15 | for jABC Release 1.9.8a |
| 0.8 | 2005-07-04 | |
| 0.3 | 2005-02-28 | |
| 0.2 | 2005-01-25 | |
| 0.1.2 | 2005-01-10 | Release for the formula builder |
| 0.1.1 | 2004-10-28 | |
| 0.1 | 2004-07-21 | |
| Type | Changes | By |
|---|
 | Game graph layouter did not work if two nodes from the original model
shared the same label. Fixes 1189. | renner |
| MacroHandler is now more robust wrt. problems during initialization
of macros. Fixes 1187. | renner |
| Models with dangling edges could not be saved. Fixes 1185. | renner |
| Fixed odd behavior of SIB marking after model checking (concurrency issue). Fixes 1085. | renner |
 | Properties attached to a model can now be managed (edit formulas or
their descriptions) from the Basic View by right-clicking on the table. Fixes 1151. | renner |
| Syntax Highlighter and auto-completion now also recognize atomic
propositions used in the model. Fixes 589. | renner |
 | The Macro information dialog has ben cleaned up. Macros can now
use more documentation options for their descriptions. Fixes 868. | renner |
| Equivalence classes are now presented in mixfix notation. The old-style symbolic expression
presentation can be enabled by setting the appropriate key in the GEAR.properties. | bakera |
| Reduced obfuscation level to fix problems with I18N data retrieval. Fixes 1152. | bakera |
| Fixed odd behaviour of the Syntax Highlighter. GEAR now uses the Jyntax
Syntax Highlighter. Highlighting is now more flexible and also works
properly for the default mixfix syntax. Fixes 1149. | renner |
| Choice of preferred syntax was sometimes reset to the prefix syntax. Fixed
a bug in the UserObject handling when no syntax preference was stored with
the model. Fixes 1148. | renner |
| Type | Changes | By |
|---|
| GEAR inspector is now automatically shown once jABC starts. No need
to explicitly start the plug-in anymore. Fixes 1140. | renner |
| SIBEXP macro is now capable of handling SIB labels. | renner |
| ID expression now references SIB-IDs instead of SIB names or SIB
labels. ID expressions should not be used anymore by anyone
but macro developers. Fixes 1053. | renner |
| User documentation moved to jABC Manual Wiki. Fixes 386. | renner |
| Mixfix syntax is now used as the default syntax. Fixes 1061. | renner |
| jABC Option "Autodefine branches" caused problems during game
graph generation. Fixes 864. | renner |
| Order of properties stored with a model should now be deterministic. Fixes 791. | renner |
| Added macro EDGECOUNT that is satisfied by all nodes having the
given number of incoming/outgoing edges. Fixes 869. | renner |
| jABC Option "Autodefine branches" caused problems during game
graph generation. Fixes 864. | renner |
| Small bugfix in Mixfix parser wrt. too many closing parentheses. Fixes 858. | bakera |
| Syntax selection menu is now less technical. Fixes 1057. | renner |
| CTL operators have changed their syntax slightly. See the user
documentation (jABC Manual Wiki) for details. | renner |
| Advanced view entry field now provides a short information about
the operators used in the formula via a tooltip. | renner |
| Added ant task for GEAR to integrate GEAR in the ant build process. Fixes 1034. | bakera |
| Game graph configuration dialog did not respect Cancel and Close
Window events properly (game graphs were built anyway). Fixes 1056. | renner |
| The macro list file is now handled differently. The old file
GEAR.macros will now be ignored. See the issue for details. Fixes 867. | renner |
| jABC game graphs now make proper use of SIB labels and names. What
formerly was used as a name is now used as a label. Regarding the
names, SIBs are now simply numbered. | renner |
| Code of modules core and GUI is now obfuscated. Fixes 883. | bakera |
| The parser treated input as valid as long it was able to parse
it. So expressions like '(a | b))' with too many closing
parenthesis were accepted. The parser is now more strict and
would reject this. Fixes 858. | bakera |
| Now it is possible to export game graphs to an instiated
version of GDL (game description language). Fixes 861. | bakera |
| There is a warning if the overlay icon option is selected for
marking satisfying SIBs but there is not overlay icon position
set in jABC's option dialog. | bakera |
| Type | Changes | By |
|---|
| Added a property to enable all BETA-level features. Those features
are not yet mature enough to be enabled by default but should
be available for testing. Set
de.metaframe.plugin.gear.GearPlugin.BETA_FEATURES_ENABLED=true in
GEAR.properties. | renner |
| GEAR now supports different types of edges - namely MAY and
MUST edges. Thus the Model interface changed. Therefore all
dependent implementatations (li
ke Nodes and Edges) changed as
well. So far all edges emerging from jABC models are assumed
to be MUST edges. Fixes 432. | bakera |
| Overall project switched to Maven. | |
| Performance improvement for the overall modelchecking
process. This was accomplished by the following
tasks. 1. Propositional Expressions are compiled into ID
expressions (reducing the size of the game
graph). 2. Recursive implementation of computation of
priorities improved. 3. GameGraph now connected in both ways
(forward and backward). Fixes 524. | bakera |
| New (hidden) menu entry to allow export of the game graph into
a GDL like representation. | bakera |
| Reestablished old mix fix style syntax (using the Java
Expression Parser) and established a new superior mix fix
syntax. | bakera |
| Type | Changes | By |
|---|
| Game graph nodes are annotated with mixfix formula notation if
desired. | renner |
| AP Manager now allows for removing, adding and setting atomic
propositions for multiple SIBs. | |
| Game graphs augmented with commonly used formulas (SIBEXPs for
common tasks). | bakera |
| Using new dialog that warns about various things and asks
about user preferences for the respective warning | renner |
| Using new Exception Frame that hides the ugly details of
exceptions and attempts to produce a user-friendly report. | |
| Markings could not be removed from game graphs. Fixes 579. | |
| Adopted the more formal notation of diamonds and boxes for
game graph nodes. | |
| Add
ed a legend for the formula manager. Fixes 519. | renner |
| Syntax Highlighter missed some tokens in lower case. Fixes 516. | renner |
| AWU/EWU-Macros enhanced by back-option | |
| Clicking on grey subformulas performs model checking and by
this reveals semantics of underivable subformulas. | |
| Atomic Propositions editable while shown instead of SIB
default icons. | bakera |
| Added fancy splash screen upon start of GEAR. | bakera |
| MacroScanner prevented GEAR from starting correctly if no
project is present | bakera |
| Incorrect property referenced in EntryFieldPopupMenu | |
| Special characters like newline or tab were not treated
correctly by the parser. | bakera |
| Not fully connected edges produce more sophisticated error
messages. | |
| Quoted atomic proposition induced problems during pushing of
negations. Fixes 473. | renner |
| Warning when graph model contains control SIBs. | bakera |
| Advanced View now automatically shows the results for the
whole formula. Fixes 509. | renner |
| "... and 0 more" in the Advanced View's entry field popup
menu. Fixes 523. | renner |
| Added mark mode in Advanced View to select satisfying SIBs. | renner |
| Type | Changes | By |
|---|
| Refactored GEAR's SIBs due to changes in the JavaABC package
structure. | |
| Entry field (auto-completion and syntax highlighting) is no
w
correctly updated when a SIB graph is added as a macro. Fixes 337. | |
| Context menu in Advanced View shows at most ten properties (by
default), the remaining properties can be inspected in the
formula manager. Fixes 479. | |
| Property list in Basic View is now scrollable. Fixes 480. | |
| CTL Until macros were not expanded correctly with fixpoint
formulas as arguments | |
| Expression Tree in Advanced view is now being updated a little
more lazy (configurable delay) | |
| New macro scanner that makes use of the SIB scanner
(technically macros are SIBs now). | |
| in the jABC preferences directory | |
| Type | Changes | By |
|---|
![]() | Adaptation to new Java ABC 3.0 class structure. | |
![]() | Added Macro LOAD to load properties from a file. | |
![]() | Macro SIBEXP now also supports selecting SIBs which have a
specific parameter by simply leaving out the range. The
expression '(SIBEXP param count)' e.g. expands to all SIBs
that have a parameter called 'count'. | |
![]() | No longer setting an icon for GEAR's inspector pane. | |
| Type | Changes | By |
|---|
![]() | Added Macro PROP to reference a stored expression via a
description. | |
![]() | All menu entries are disabled until the plugin has been
started. | |
| Generated Scripts to be applied to SIBs were malformed. | |
![]() | Macro information page
updated. | |
![]() | Added macro LOCALCHECK to provide local checking information
in model checking formulas. | |
![]() | Added macros for specification patterns (see
http://patterns.projects.cis.ksu.edu/) | |
![]() | Extended the SIB inspection macros (now called SIBEXP) to
support regular expressions, variables, more comparison
operators for accessing SIB parameters, access to SIB instance
names as well as access to branches of a SIB. | |
![]() | Added implicit operation macros BIGOR and BIGAND that can be
used in connection with SIB expressions. | |
![]() | Added REGEXP macro for selecting all nodes with atomic
propositions matching a specific regular expression (can also
be embedded into SIB expressions and PREDS/SUCCS). | |
![]() | Added PREDS and SUCCS which are alternatives for forward and
backward variants of BOX and DIA supporting branch complements
(with NOT) as well as regular expressions. | |
| Some gamegraphs were corupted by computation of winning
strategies. | |
![]() | Added macros for PDL (Propositional Dynamic Logic) support. | |
![]() | Added macro IFX to support infix notation for formulas. | |
| Branch labels with white space weren't considered correctly. | |
![]() | ModelMacro interface for implementation of macros has been
changed. Now both expanded and unexpanded operands will be
handed into the macro. | |
![]() | Removed menu: 'SIB parameter as propositions'. Use macros
(e.g. SIBEXP) for this. | |
![]() | Edges without any branch labels can be model checked. | |
![]() | The formula tree has been cleaned up. | |
| Problem with locales on Windows machines fixed. | |
![]() | Macro EXPAND now able to expand model unboundedly. | |
![]() | Command line interface and plugin are searching the classpath
for macros. | |
![]() | Macros AG, EG, AF, EF extended with parameters to specify
scope (finite vs. infinite) and direction (forward
vs. backward). | |
![]() | Atomic propositions and node names may be masked in
expressions with '"'. | |
![]() | Added Macro (SEL) expanding into currently selected cells. | |
| Negations of IDs were not transformed properly into positive
form (node names containing spaces). | |
![]() | Added Macro (EMLEI) that implements the Emerson-Lei
model-checking algorithm. | |
| Game graphs can be executed via the Tracer (2.0). The games
can be viewed now, but not really played. | |
| Game graph layouting did not work in some cases with branch
constraints. | |
![]() | A new multi-line formula editor for longer formulas is now
available (entry field context menu). | |
![]() | New traceable SIB for game graph generation. | |
| Auto-completion hindered formula entry (popup on parentheses). | |
![]() | The formula manager has received a complete redesign. | |
![]() | Command-line interface has been removed. Simple command lines
are only available for jETI integration. | |
| Type | Changes | By |
|---|
![]() | Created some SIBs to perform Model Checking. | |
![]() | New macro mechanism capable of enhanci
ng the syntax with
arbitrary operators (even actual alternative model-checking
algorithms), thus turning GEAR into a model-checking
framework. | |
![]() | CTL operators implemented as macros. | |
| Formula manager can now be opened only once per model. | |
![]() | New mechanism to handle GraphSIB expansions: expansions can
now be performed once, bounded or unbounded and will be
handled by some Macro EXPAND. | |
![]() | Formula entry field now supports semi-auto-completion with
CTRL+SPACE and popups on opening parenthesis. | |
| Right mouse button did not work properly in some Macintosh
scenarios. | |
![]() | instead. | |
![]() | some helper for expression entry field inserting ')' each time
a '(' is inserted. | |
![]() | Parsing interactively during input of expression such that
expression tree evolves while typing the expression. | |
![]() | Changed Parser syntax to new prefix oriented notation of
symbolic expressions. Some abbreviation for quotation macro
QUOTE as ' introduced. | |
![]() | Added Menu entry to automatically scan for macros and to
display information about registered Macros. | |
![]() | Command-line parameter --expand deprecated. Use the EXPAND
macro instead. | |
![]() | Internationalization moved from Java classes to properties
files. | |
![]() | Added Menu entry for syntax/grammar help to plugin menu. | |
![]() | Model Interface no longer supports types of node and edge
labels but assumes Strings in both cases. New method
getIdentifier
() introduced. | |
![]() | Removed links from this about page. | |
![]() | Interface Model no longer extends iterable. So there is no
more need to implement method iterator. | |
![]() | GEAR split up in two modules: core and gui. | |
| Type | Changes | By |
|---|
![]() | New menu entry to insert a smaller variant of a game graph
thats not playable but can be saved. | |
![]() | New abbreviations for CTL operators UNTIL: EWU=EW, AWU=AW,
ESU=EU, ASU=AU. | |
![]() | New menu entry to allow SIB names to be considered as extra
atomic propositions. | |
| Exception when using an additional SIB parameter that is not
present on all SIBs. Fixes 72. | |
| Copying graph properties between models lead to a hang. Fixes 61. | |
![]() | When entering a new formula, the formula itself is used as its
preliminary description (until the user enters a different
description). | |
| Continuous checking in the Basic view improved: Checking on
activation of different model as well as when the checkbox is
ticked. | |
| Changed error message when GraphSIBs should be expanded and
the referenced model is not present. Fixes 71. | |
| Type | Changes | By |
|---|
| Continuous checking in the basic view did not respond to model
changes. | |
![]() | Changed constructor for AssemblyLine to usage of enums. Old
(now deprecated) constructor still there but produces
warnings. | |
![]() | The interface for applying code to sibs t
hat satisfy the given
formula has been redesigned. Buttons have been transferred to
menus. A menu to create sample scripts has been added. | |
| Transformation into positive form (negations only directly
before propositions) corrected for MIN/MAX fixpoints. | |
![]() | Added a short README.TXT to the distribution directory that
holds some short information about the plugin, the JARs
involved and a reference to the homepage for more information. | |
| Pressing RETURN after inserting a malformed formula into the
formula entry field caused a dialog box to be opened. Leaving
this dialog by pressing RETURN again caused the entry field to
check the formula again and opened the error dialog again. Ad
infinitum. | |
| Implicitely inifite models (by recursive usage of graph SIBs)
lead to a hung. Fixed this by showing an error to the user and
aborting the expansion process. | |
| GEAR got a new icon. | |
| Selecting branch constraints in the formula tree caused
exceptions. Fixed this: Now branch holding this constraint
will be selected. | |
![]() | CSV-Model (a sample implementation of model-checkable model
besides the SIB Graph Model) revived. | |
![]() | Reviewed documentation (to be found now as PDF inside the
plugin jar) and extended it with a developer guide introducing
some concepts of usage, implementation details, and example
implementations. | |
| Type | Changes | By |
|---|
| Popup menu (right-click on canvas) would hang when Graph
contains GraphSIBs. Fixes 39. | |
![]() | Some more internationalization (popup menu). | |
| Type | Changes | By |
|---|
![]() | AP view now additionally contains propositions fetched from
SIB parameters and hidden propositions (e.g. those generated
by the FormulaBuilder). | |
| Simple formulas like BOX(true) haven't been considered
correctly. Fixed this problem. | |
| Annoyance fixed: CLI did not terminate due to GUI dependencies | |
![]() | Separated core logic from GUI (JavaABC plugin) | |
![]() | New video tutorials for copying graph properties and showing
atomic propositions. | |
![]() | German translation updated | |
| Type | Changes | By |
|---|
![]() | Deleted commandline option --sibfolder because the sib loader
will only look into the classpath. | |
![]() | Commandline interface extended by two new parameters --expand
and --refModel to handle graph SIBs. | |
![]() | New menu entry to switch between different viewsof the SIB
Graph - one to show the SIB Graph as it is and one to show
atomic propositions instead of icons. | |
![]() | Some new options exported to the properties file which have
been handled otherwise before. | |
![]() | Introduced new menu entry to handle GraphSIBs. | |
![]() | AssemblyLine needs information about expansion of GraphSIBs
now. | |
![]() | When invoked by command line no properties will be stored
anymore. | |
![]() | Graph SIBs will be expanded if desired. A graph SIB is called
to satisfy whenever all referencing models (directly or
indirectly) satisfy. | |
![]() | If no SIB is selected the AP
-Manager will show up propositions
of all nodes in the current model. | |
![]() | Integrated mc-specific properties file into jABC
properties. Options Dialog no longer needed and removed. | |
![]() | Icons introduced at top of inspector panes. | |
![]() | Formulas will be parsed while entering into the entryfield and
correct syntax is indicated by coloring the background of the
entryfield.. | |
![]() | Integrating JUnit and performing many tests now. | |
![]() | Bean shell script associated with SIB Graph dynamicly changes
in script window while changing the model. | |
![]() | New buttons to select all/none of the model properties in the
Basic View. | |
| Type | Changes | By |
|---|
![]() | Menu entry for Clarke's algorithm disabled by default - may be
turned on again in the modelchecking properties file if
needed. | |
![]() | Copying of properties between graphs supported by new menu
entry. | |
![]() | Model checking plugin now available as standalone version to
be used from the command line. | |
![]() | Command line interface has been extended by the paramter
--formulafile to give a file with formulas to be considered. | |
![]() | Code to be applied to satisfying SIBs will be stored with the
SIB graph file. | |
| Type | Changes | By |
|---|
![]() | Online help can now be found inside the jar. | |
![]() | Games can be played by clicking game graph nodes inside the
game graph. Nodes playable by the user are marked with a
smiley, nodes played by the computer are marked wi
th a
calculator. The user has to find out whether a game is won or
not at the moment. | |
![]() | Redesign of Handling of Atomic Propositions: SIBs don't need
to implement an interface anymore. Modelchecking information
is now stored in the user object of SIBs at the keys found in
de.metaframe.plugin.gear.UserObjectKeys. | |
![]() | Atomic propositions may now be managed with the AP-Manager
inspector. Enter propositions - one at a line - and/or choose
a SIB parameter to be chosen additionaly for atomic
propositions. | |
![]() | BOX_BACK and DIA_BACK now supported for Yoo's and Clarke's
algorithm. | |
![]() | A command line interface has been introduced in the class
MCCLI (ModelCheckingCommandLineInterface). Help about usage
may be found by invoking it without any arguments or with
--help. | |
![]() | About window contains clickable links for more information
about new features. | |
![]() | New Basic Model Checking inspector for users not familiar with
formal logic. The inspector displays descriptions instead of
formulas and allows explicit checking or the contiguous
inspection of the current model. Formulas still have to be
associated with models via the "classic" inspector or formula
manager. | |
| Type | Changes | By |
|---|
| Descriptions for stored formulas were accidentally removed
sometimes. | |
![]() | A new menu entry was introduced to set a SIB paramter to be a
fall back for atomic propositions. Set it to a SIB parameter
and the modelchecker will receive its atomics proposition from
this paramter. If the paramter is a collection, all entries
of the collection were used as atomic propositions. | |
![]() | The c
onfigure panel to configure icon locations has been
removed due to clean code. | |
![]() | Selecting more than one cell in the sib graph while marking
error paths will result into markings of all error paths
starting from the selected nodes. | |
![]() | Inspector redesign with toolbar at the bottom of the panel --
new funny icons. | |
| Update of properties file caused Java ABC to hang | |
| Type | Changes | By |
|---|
![]() | Branches will be highlighted for BOX/DIA operators upon
clicking the branch constraints. | |
![]() | Multiple formulas (along with descriptions) can be saved with
the SIB graph. | |
![]() | Stored formulas can be managed/deleted upon right-click into
the formula entry field. | |
![]() | Syntax highlighter for formula entry field now recognizes
"true" and "false" atomic propositons. | |
![]() | Migrated to java 1.5. | |
![]() | Popup menu on SIBs introduced. | |
![]() | About menu with version history introduced. | |
![]() | Modelchecking adds some SIBs to every project to guarantee
their presence at creation time of the game graph | |
| Bugfix in conversion from CTL to mu-calculus (nested fixed
points now working again) | |
![]() | Complete update of online documentation | |
![]() | Error Paths will be highlighted upon right clicking a SIB and
chosing "show error path" inside the modelchecking sub menu. | |
![]() | Highlighting color and line thickness of error paths can be
configured in the jABC options dialog. | |
| Type | Changes | By |
|---|
![]() | Model checker now usable without gui via the class
de.metaframe.plugin.gear.AssemblyLine. | |
![]() | AWU and EWU introduced. | |
![]() | Negations only supported right before atomic propositions
(using positive form). | |
![]() | A new menu was introduced to apply some (beanshell) code to
SIBs that satisfy a modelchecking condition. | |
![]() | More shortcuts for menu entries introduced. | |
![]() | Modelchecking controls can be put inside a seperate window
instead of using the inspector pane of jABC. | |
![]() | Plugin checks compatibility with version of jABC. | |
![]() | More messages inside the status bar. | |
| Bugfix in default properties file. | |
| Type | Changes | By |
|---|
![]() | new operators ASU, ESU | |
![]() | new CSV-model implemented | |
![]() | a lot of tests for validation | |
![]() | introducing real game graphs | |
![]() | CTL operators are no longer handled by themself. They are
simply converted into formulas of modal mu-calculus. | |
| Type | Changes | By |
|---|
| Minor bugfixes in the CTL section. | |
![]() | javadoc reviewed | |
![]() | new implementation of a simple model - different from the
SIBGraph model | |
![]() | marking edges in model | |
![]() | marking SIBs results in marking subformulas when semantics of
the subformula contain this SIB. | |
![]() | basic syntax highlighting for formulas | |
![]() | some options can be configured by a dialog (no save support) | |
| Type | Changes | By |
|---|
![]() | Added game graph in tabular and graphical representation | |
| Bugfix of CTL operators for non-complete graphs | |
![]() | Two atomic propositions true and false (ignore case)
introduced | |
![]() | BOX_BACK und DIA_BACK as backward variants of BOX and DIA
added | |
![]() | IMP for logical implications | |
| Type | Changes | By |
|---|
| Some minor bugfixes. | |
![]() | Changing SIBGraph model to a more general model. | |
| Type | Changes | By |
|---|
![]() | some icons used instead of text buttons | |
![]() | added help | |
![]() | I18N for English and German | |
![]() | modelchecking using SIB names | |
| Type | Changes | By |
|---|
![]() | basic modelchecking using CTL, mu-calculus | |
