------------------------------------------------------------------------------ CHANGES Change history of RISCAL. Author: Wolfgang Schreiner Copyright (C) 2016-, Research Institute for Symbolic Computation (RISC) Johannes Kepler University, Linz, Austria, http://www.risc.jku.at This program is free software: you can redistribute it and/or modify it under the terms of the GNU General Public License as published by the Free Software Foundation, either version 3 of the License, or (at your option) any later version. This program is distributed in the hope that it will be useful, but WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License for more details. You should have received a copy of the GNU General Public License along with this program. If not, see . ------------------------------------------------------------------------------ 4.2.7 (July 3, 2023) Performance improvements and bug fixes in system invariant/LTL checking. 4.2.6 (June 22, 2023) Bundled with eclipse-2023-06 packages, switch to Java 17. 4.2.5 (May 9, 2023) Bug fixes in LTL checker, counterexamples constrained by "Depth" field. 4.2.4 (March 8, 2023) Introduce command-line option "-el" for LTL formula checking. 4.2.3 (December 23, 2022) Add window size calculation to accommodate HiDPI displays. 4.2.2 (September 16, 2022) Integration with RISCTP 1.3.1. 4.2.1 (September 12, 2022) Bug fix in LTL model checker and type checker. 4.2.0 (September 6, 2022) LTL model checker by Ágoston Sütő. 4.1.3 (July 26, 2022) Multi-threaded version of invariant checking for nondeterministic systems. 4.1.2 (July 22, 2022) Improved theorem proving by "choose[sat]" expressions of RISCTP 1.3. 4.1.1 (July 15, 2022) Add missing preconditions to RISCTP translation of procedures. 4.1 (July 11, 2022) Integration with RISCTP 1.2, theorem proving binding for cvc5 and Vampire. 4.0 (July 7, 2022) Integration with the RISCTP theorem proving interface. Bundled with eclipse-2022-06 packages (including GEF 5.4.0). 3.8.9 (June 7, 2022) Added "fairness3" clause to LTL specs and fairness predicates to LTL language. 3.8.8 (February 3, 2022) Changed LTL tokens and keywords to avoid conflicts with existing specs. 3.8.7 (October 21, 2021) Bundled with eclipse-2021-09 packages (but stay with GEF 5.3.1, newer versions have problems with node interaction). Prepare framework for LTL model checking. 3.8.6 (June 1, 2021) Fix bugs in time reporting and inlining function applications. 3.8.5 (May 20, 2021) Refine scope of inlining in "eliminate choices". 3.8.4 (May 18, 2021) Add missing contract expansion to calls of recursive functions. 3.8.3 (May 17, 2021) Add missing contract expansion to procedure tasks. 3.8.2 (May 17, 2021) Revise implementation of "eliminate choices". Make "inline definitions" separate option. 3.8.1 (May 6, 2021) Inline definitions for option "eliminate choose expressions". 3.8.0 (May 5, 2021) Add SMT option "eliminate choose expressions". Disable loading and saving options in non-interactive mode. Fix minor bug in file dialog. 3.7.5 (April 26, 2021) Fix bug in "systems" processing. 3.7.4 (April 21, 2021) Fix bug in "Save As" dialog. 3.7.3 (March 31, 2021) Minor SMT bug fix. 3.7.2 (March 11, 2021) Store root of state tree to speed up system invariant checking. 3.7.1 (February 23, 2021) Print time also for error execution. 3.7.0 (November 23, 2020) Generate verification conditions for systems, SMT bug fix. 3.6.2 (September 22, 2020) Bundled with eclipse-2020-09 packages, get rid of scrollbar bug. 3.6.1 (September 9, 2020) Fix bug in initialization expressions of shared systems. 3.6.0 (July 31, 2020) Introduction of "printtrace" command and expression. 3.5.2 (July 22, 2020) Minor fixes, clarification in manual about applying SMT to VCs. 3.5.1 (July 8, 2020) Bundled with eclipse-2020-06 packages. 3.5.0 (July 7, 2020) Fix incorrect verification condition generation for block commands. Fix minor bug in verification condition annotation. Fix minor bug in non-deterministic evaluation of for-in loops. 3.4.9 (July 2, 2020) Minor bug fix in SMT translation. 3.4.8 (June 25, 2020) Bug fix in SMT translation of min/max. 3.4.7 (June 24, 2020) Bug fix in nondeterministic evaluation of let expressions. 3.4.6 (June 24, 2020) Improvement of SMT translation of min/max. Minor bug fixes in choice guard and precondition generation. 3.4.5 (June 23, 2020) Explicit SMT translation of min/max. Fix minor bugs in type checking/evaluating power expressions. 3.4.4 (June 10, 2020) Fix minor bug in type checker with respect to subtypes. 3.4.3 (June 9, 2020) Fix bug in SMT guard checks. 3.4.2 (June 9, 2020) Minor fix in "check" command. 3.4.1 (May 27, 2020) Fix wrong computation of "Union {}". 3.4 (May 25, 2020) Add SMT option "check iteratively". Fix bug in invariants for for-loops. 3.3.1 (May 20, 2020) Fix GUI bug ("Restore Defaults" did not consider choice guards) 3.3 (May 19, 2020) Add SMT option "check dependencies". Revert/correct bug fix in loop annotations introduced in 3.2. Remove problemantic form of array and map builders introduced in 3.1. 3.2 (May 18, 2020) Experimental support for SMT-LIB quantifiers. Fix bug in invariants for for/choose-loops. 3.1.1 (May 14, 2020) Application of SMT solver to task folders, operations notin and notsubseteq). 3.1 (April 28, 2020) Simplified array and map builders, make CTRL-# work for Windows. 3.0 (April 8, 2020) New language feature "distributed systems", minor SMT bug fix. 2.12.2 (April 1, 2020) Minor bug fixes (verification conditions, semantics, power expressions). 2.12.1 (March 31, 2020) Minor SMT bug fix, update of manual. 2.12.0 (March 23, 2020) SMT bug fixes, new option "choice guards". New language feature "shared systems". 2.11.0 (February 18, 2020) SMT extension by Franz-Xaver Reichl. Minor bug fixes (execution of multi-variable quantifiers, context sizes). 2.10.5 (December 3, 2019) Minor bug fixes (unique ids of refutations, assignments to subtyped arrays) 2.10.4 (November 4, 2019) Minor bug fixes (depth check for recursive types, domain sizes of sets) 2.10.3 (October 1, 2019) Fix invalid type combination rules for maps. 2.10.2 (September 24, 2019) Add missing fix for non-UFT8 systems (Windows). 2.10.1 (September 19, 2019) Make UTF8 encoding explicit for use on non-UTF8 systems (Windows). Introduce environment variables for font selection. 2.10.0 (August 29, 2019) Introduce button and menu entry for list of symbols. Introduce array builder syntax with multiple initialization values. Add missing preconditions for initialization values in array/map builders. Add missing binder for "old" variables in loop verification conditions. 2.9.3 (August 1, 2019) Fix bug in non-deterministic handling of binders. 2.9.2 (July 30, 2019) Fix bug in computation of a*..*b and n!. Fix missing effect of "modular" in function applications in contracts. Disallow "ensures" clauses in theorems and axioms. 2.9.1 (July 16, 2019) Bundled with eclipse-2019-06 packages. 2.9.0 (May 21, 2019) Strengthen well-definedness condition of loop invariants. Strengthen semantics of "choose-else" commands and expressions. 2.8.0 (May 20, 2019) Add task menu entry "Show Counterexample". Add new variant of "check" command and of "print in" command. 2.7.3 (April 26, 2019) Fix bug in handling record types within recursive types. 2.7.2 (March 15, 2019) Fix bug in runtime type checking of selector updates. 2.7.1 (March 13, 2019) Fix bug in semantics of "choose-else" command 2.7.0 (March 11, 2019) Add entry "Execute All Tasks" to pop-up menu of task folders. 2.6.6 (February 28, 2019) Fix minor bugs in verification condition generation. 2.6.5 (February 25, 2019) Give more informative error messages for violated pre/postconditions. Fix minor bug in verification condition generation. Fix minor bug in progress bar computation in multi-threaded mode. Correct documentation for "modular" clause. Bundled with eclipse-2018-12 packages. 2.6.4 (December 10, 2018) Minor changes in visualization of formula evaluation. 2.6.3 (November 29, 2018) Fix evaluation order of "print ... in ..." expression. 2.6.2 (November 29, 2018) Fix bug in free variable computation/minimization of "with" clause. 2.6.1 (October 18, 2018) Fix bug in verification condition for "check" command. 2.6.0 (October 17, 2018) Fix bug in trace visualization, revise command line options. 2.5.1 (October 8, 2018) Fix bug in test for recursive types. 2.5.0 (October 4, 2018) Introduce command line options for non-interactive use. Fix performance penalties introduced in versions 2.1.0 and 2.4.0. 2.4.0 (September 25, 2018) Introduce quantified variables with multiple filter predicates. Fix bug in non-deterministic evaluation of quantified variables. Increase bound on ANTLR's error recovery attempts introduced in 2.3.0 2.3.1 (September 20, 2018) Bundled with eclipse 2018-09 packages, document Java 11 compatibility. 2.3.0 (September 18, 2018) Allow builtin type constructors in recursive types. Introduce "axiom" declarations. Prevent ANTLR's error recovery to sometimes run into infinite(?) loops. Fix number of local threads used when distributed option is selected. Improve handling of "abort" button. 2.2.0 (September 12, 2018) Introduce function "height" on recursive types. Package with ANTLR 4.7. 2.1.3 (August 14, 2018) Bug fixes (verification conditions for record updates) 2.1.2 (August 13, 2018) Bug fix (crash in verification condition generation for record updates) 2.1.1 (August 1, 2018) Bug fixes (crash in vcg, processing of saved files, user interface glitches) 2.1.0 (July 17, 2018) Visualization of evaluation trees. 2.0.2 (June 28, 2018) Packaged with SWT 4.8. 2.0.1 (June 27, 2018) Fix minor bug in type checking verification conditions. 2.0 (June 18, 2018) Introduce verification condition generator. 1.0.17 (April 30, 2018) Fix bug in type checking array builder expressions. 1.0.16 (March 29, 2018) Add optional visualization of execution traces of procedures. 1.0.15 (March 21, 2018) Fix bug in handling record types. 1.0.14 (January 15, 2018) Suppress specification validation tasks in operation menu. 1.0.13 (December 11, 2017) Fix bug for specification validation with remote servers. 1.0.12 (November 15, 2017) Added specification validation tasks, minor bug fixes. 1.0.11 (October 23, 2017) Minor bug fixes. 1.0.10 (October 16, 2017) Print result on postcondition violation, minor improvements. 1.0.9 (October 11, 2017) Fixed user interface glitch, packaged with SVN 4.7.1a. 1.0.8 (October 4, 2017) Fixed performance bug (excessive progress bar updates) 1.0.7 (September 26, 2017) Introduction of subtypes. Associated rewriting of size computation of types. Bug fix in slot allocation for result variable of functions. 1.0.6 (September 4, 2017) Extend choose expression to multiple variables. 1.0.5 (August 1, 2017) Minor bug fix (choose in non-deterministic mode) 1.0.4 (July 4, 2017) Minor bug fix (handling of special name "result") Packaged with SWT 4.7 1.0.3 (March 28, 2017) Minor bug fixes (recursive types, error message on premature eof) 1.0.2 (March 20, 2017) Minor bug fixes (type checker, more lazy choice, catch stack overflow) 1.0.1 (March 17, 2017) Minor bug fixes (file saving, thread number). 1.0 (March 1, 2017) First release. ------------------------------------------------------------------------------ End of CHANGES. ------------------------------------------------------------------------------