v0.1.9
Pre-release
Pre-release
Features
Ultimate.py wrapper script cli arguments:
--data <directory>
can be used to specify the data directory (location for temporary files) (close #115)--config <directory>
can be used to specify the directory in which settings (.epf) and toolchain (.xml) files are stored (close #114)--witness-dir <dir>
and--witness-name <string>
allows you to specify to where the correctness or violation witness is written (close #116)- all cli arguments are now non-positional
init()
-clause is now extracted from .prp files and passed as parameter to Ultimate (close #117)- LTL formulas are extracted from .prp files and converted to Ultimate input files (.ltl) if necessary (close #118)
BlockEncoding
- SBE and rewriting (dis)equalities for transformulas (closes #134)
- replaced BlockEncoding with BlockEncodingV2 in all toolchains
- LTLautomizer uses LBE/SBE again
PathInvariantsGenerator
can use SBE/LBE for path programs (closes #108)
AutomataLib
- added a new mode "DYNAMIC" (default) that uses the complete test based on heuristics
Error messages and log messages
- provide information if some perfect interpolant sequence was found
- Core does not add timeout result if plugin already added timeout result
- various error messages improved
Statistics
- optionally report a BenchmarkResult for every round
- show statistics information on timeout
- also use .csv data from StatisticsData.class
- improved statistics for Automata Minimization, FullMultipebble
- new statistics AutomataOperationStatistics, ConstraintsSolvingTime, ConstraintsConstructionTime, ProgramLocsLbe
- MotzkinTransformations, DAGTreeSize separately for normal and under and/or overapproximation constraints
- number of Motzkincoefficients
- separate ProgramSize into ProgramSizeConjuncts and ProgramSizeDisjuncts
Misc
- new plugin
InvariantSynthesis
- now supporting analysis of hybrid systems with
SpaceExParser
- new transformula transformation for modulo operations:
ModuloNeighborTransformation
- PathPrograms can be extracted from ICFG and written to .bpl file
- Hoare-Triple-Checker based on abstract interpretation implemented (see #109)
- added support for float macros
fpclassify
andisnormal
frommath.h
- added generalization of counter examples in TreeAutomizer
- Updated website / webinterface
- Updated various default settings
Bugfixes
- transformula transformation
RemoveNegation
makes "best effort" when removing negations instead of crashing - fix ltlautomizer bug (always trivially satisfied)
- fix webinterface deployment
- fix "always debug logging in gui" bug
- plugin implementing multiple extension points is listed only once (closes #70)
- fix bug in
IcfgLocationIterator
which lead to duplicate states in stream if an initial node can be visited multiple times (closes #130), same forIcfgEdgeIterator
- fix various memory leaks in test framework that occurred after introduction of non-static handling of
AfterClass
directives (explicitly freeing pointers) (see #132) - fix incomplete Buchi language equivalence check was unsound
- various fixes for PMaxSAT and other automata operations
- fix size computation in
PartitionBackedSetOfPairs
Plumbing
Project ICFG of the future
- replaced dependencies to
BoogieIcfgLocation
,Call
,Return
,Codeblock
withIcfgLocation
,IAction
,IICfgTransition
counterparts all over the place - fix Kojak compatibility with IIcfg
- remove
IType
fromBoogieVar
- cleanup
RankVarConstructor
- remove methods for construction of auxiliary variables in Boogie to SMT conversion
- add method for construction of global program variables in
ProgramVarUtils
- refactoring: construction of auxiliary rankvars does not modify original symbol table
Testing
- enable non-static after class methods in JUnit to get rid of static incremental logs and summaries (prevents conflicts during parallel test execution because of back references to core/service instances)
- added testsuite describing Taipan vs Automizer differences in SVCOMP17 (based on Marius' script, closes #133)
- added LTLAutomizer regression test suite (closes #110)
- added
IFailedAnalysisResult
to group failure results - added
NoErrorTestResultDecider
that fails if we provide no analysis result for any reason except timeout - clearer regex handling in regression test suite (having include and exclude regexes that behave as expected) (73a223f)
Misc
ILocation
is an annotation,ILocation#getOrigin
is removed- introduced infrastructure for merging annotations (especially locations), merge locations during block encoding
- allow
IController
to accessIToolchainStorage
before toolchain execution viaIController#prerun
callback - new feature for preferences: register preference layers (via
IUltimateServiceProvider#registerPreferenceLayer(Class<?> creator, String... pluginIds)
) that allow you to temporarily overwrite preferences - introduced
TransforumlaTransformationResult
to represent overapproximations during transformula transformation (closes #127) - refactoring of
IStateFactory
and cleanup of AutomataLibrary - fixed most of the Sonar issues for TreeAutomizer
- added external binaries (z3, mathsat, cvc4, ...) to repository in default/adds directory and use them during deployment (necessary for Distress)
Known Issues
Hoare-Triple-Checker based on abstract interpretation has still some bugs (see #109)
README and Website usage instructions still outdated (see #135)