Allow closing of multiple tabs in mcrl2xi

2012-11-13 07:51:16: @jkeiren commented

(In r11380) Merge all revisions up to r11353 from trunk.

Detailed descriptions follow:

Temporarily disable sanity check

Added explicit representation of pbes in PFNF format (untested).
Implemented control flow algorithm in terms of pfnf_pbes.

Conflicts:

libraries/pbes/include/mcrl2/pbes/detail/control_flow.h

Fixed an lps2lts summand pruning bug that would produce incorrect state spaces in particular situations; added debug checks to the shared_subset data structure.

Fixes #1016

Applied simplification of a pbes as a preprocessing step, instead of on the fly.
Added a function for computing rule parameters.

(mCRL2-gui-qt) Partially implemented reading of tool options.

Made a start with the new implementation of alphabet reduction. N.B. Incomplete and untested!
Applied some fixes to alphabet reduction.
Added a test.

(mCRL2-gui-qt) Implemented reading of tool options including GUI.

Added computation of control flow parameters.

The value for far clipping was less than the value for near clipping.

Resolves #1028

Typo

ltsview-qt: properly solved bug #1028.

Fixed a problem with trace saving in lps2lts; fixed a problem with divergence detection.

Fix build

Added a mapping of process identifiers to their corresponding bodies as an input parameter to alphabet reduction.
Added support for the case that A is the set of all multi action names.
Implemented alphabet_block traverser.
Implemented hide and rename. There are two unhandled cases left in the algorithm, where an infinite set appears.
Adapted the alphabet algorithm such that alphabet_sub and alphabet_block do not have to deal with infinite sets anymore (with the help of Jan Friso).
Applied rewriting of propositional variable parameters before computing the control flow parameters.

(mCRL2-gui-qt) Implemented FilePicker and ToolValue classes.

(mCRL2-gui-qt) Implemented execution of instances.

(mCRL2-gui-qt) Finished implementation.

Put common code in class default_alphabet_traverser.

Fix Boost configuration.

Use CMake internals to handle configuring Boost. This fixes an issue spotted by Axel Belinfante on scientific Linux, with cmake 2.8.8 and boost 1.41.

Started the diagraphica-qt port as a fork of diagraphica.

diagraphica-qt: minor aesthetic changes.

Added Qt base dependencies to diagraphica-qt.

(mCRL2-gui-qt) Requested improvements.

(mCRL2-gui-qt) Implemented additional requested features.

Fixed issue #1030. The current behavior of the enumerate_quantifiers rewriter in combination with the option enumerate_finite_sorts = false was that a quantifier was only entered if it contained at least one finite quantifier variable. For example 'forall t:Real, b:Bool. phi' would be rewritten, but not 'forall t:Real. forall b:Bool. phi'. This has been fixed by also going into the recursion when all quantifier variables have infinite sorts.
Added a to_string function to map_substitution.
Added some debug print statements to enumerate_quantifiers.
Fixed clang compilation.
Fixed unused variable warning.
Added random test for pbesrewr.
Fixed issue #1031. Not all name clashes were detected due to a silly mistake: the intersection between a set and a variable_list was computed using std::set_intersection. This did not work, since the precondition of std::set_intersection (sorted input sequences) was violated.
Fixed compilation when the flag MCRL2_PFNF_VISITOR_DEBUG is defined.

(LTSGraph-qt) Implemented TikZ rendering.

Resolves #1027

(LTSGraph-qt) Fixed moving edges while moving a node. Implemented error handling for graph loading.

Resolves #1025

Fixed issue #1032. When a linear process has no summands, it is not printed as 'delta @ 0'. Apparently there is an implicit assumption that an empty linear process equals 'delta @ 0'. It seems more logical to represent this case explicitly using a deadlock summand.
Documented the convention that a linear process without any summands represents the process 'delta @ 0'.
Added missing include directory

diagraphica-qt: Prepared header files for Qt components.

diagraphica-qt: Removed defunct continuous attribute functionality and assorted partitioning code.

(mCRL2xi-qt) Improved disabled color implementation.

diagraphica-qt: Removed ColorRGB data structure in favour of QColor.

(Diagraphica-qt) Fixed windows build.

Add test case for bug #1019.

Duplicate lps2lts_test.

lps2lts_test_old contains the tests for the old implementation, lps2lts_test uses the new implementation by Ruud Koolen.

Conflicts:

libraries/lts/test/lps2lts_test.cpp

Fix bug in parsing of a linear process specification.

After parsing, the data specification needs to be made complete, to include standard data types.

Spotted using the test for bug #1019

(Diagraphica-qt) Minor windows janitorial for Ruud.

Fix unused variable warnings caught by clang 3.1

Add the undefining of nil to workarounds.h.

Actually, this is an Apple specific workaround, and needs to be treated as such. Include workarounds.h in the the standard data types during generation (list.h depends on this).

Conflicts:

libraries/data/include/mcrl2/data/list.h
tools/lpsparelm/CMakeLists.txt

Fix append warning (clang 3.1 -Wstring-plus-int)

Fix unused variable warnings (found by clang 3.1)

Add test for bug #1033.

For an empty (i.e. default constructed) aterm_balanced_tree, begin() is not equal to end(), which in the end leads to the iteration of invalid memory. Show that for an empty list the equality does hold.

Conflicts:

libraries/atermpp/test/aterm_balanced_tree_test.cpp
libraries/atermpp/test/aterm_list_test.cpp

Add warning upon initialisation of nextstate generator with timed specification.

Fixes #1034

Removed an erroneous check that was added to generated code. If we want to prevent a list to be empty, this has to be enforced in the internal format, not in the soundness checks.

Conflicts:

libraries/core/include/mcrl2/core/detail/struct_core.h

Fix build of compiling rewriter (broken in r10737)

Move workaround.h to mcrl2/utilities
Move exception.h to mcrl2/utilities

Conflicts:

libraries/bes/include/mcrl2/bes/detail/standard_form_traverser.h
libraries/core/include/mcrl2/core/detail/aterm_io.h
libraries/data/include/mcrl2/data/data_expression.h
libraries/data/source/detail/rewrite/jitty.cpp
libraries/lps/include/mcrl2/lps/detail/linear_process_conversion_traverser.h
libraries/lts/include/mcrl2/lts/detail/bithashtable.h
tools/lpsparelm/CMakeLists.txt
tools/ltsinfo/ltsinfo.cpp
tools/mcrl2-gui-qt/CMakeLists.txt

Rewrote the alphabet reduction algorithm, such that it does one recursion over a process expression and a set of multi action names, instead of two independent recursions. A few cases are still missing.
Added documentation for alphabet reduction. N.B. Some entries are still missing, or need to be checked for correctness.
Fixed issue #1033. The term_balanced_tree_iterator was broken in the sense that the default constructor and construction with an empty tree produced unequal values. This has been repaired by modifying the equal function of term_balanced_tree_iterator, such than an empty tree stack is considered equal to a stack containing an empty tree.

diagraphica-qt: Removed redundant diagram-rendering code.

Add missing include path (needed for MSVC)

(Diagraphica-qt) Fixed build and started cleanup of arcdiagram.cpp.

(Diagraphica-qt) Partial cleanup of arcdiagram and visutils.

Fix build

Made an empty domain optimization in optimized_forall/exists explicit, to prevent user errors.
Removal of unused quantifier variables is now always done inside optimized_forall/exists.
Updated occurrences of optimized_forall/exists accordingly.
Fixed a set intersection function in data_sequence_algorithm.h that had been misnamed in the past. This fixes issue #1035.

Conflicts:

libraries/data/include/mcrl2/data/detail/data_sequence_algorithm.h

Reverted the change to test case 11 of pbesconstelm, made in revision 10650. In that revision an error was introduced in the simplifying rewriter that accidentally led to a stronger result.

(Diagraphica-qt) Cleanup of arcdiagram.

(Diagraphica-qt) Cleanup of bundle.

(Diagraphica-qt) Cleanup of cluster.

(Diagraphica-qt) Cleanup of edge.

(Diagraphica-qt) Cleanup of examiner.

(Diagraphica-qt) Removed unused bitmappanel and fixed compiler warning.

(Diagraphica-qt) Partial cleanup of parser.

Added computation of control flow graph vertices.

(Diagraphica-qt) Improved writeFSMFile of parser.

Restriction loosened to undef nil

Outcommented an test for the APPLE keyword, as it does not seem to work on a 32bit apple with gcc. This makes the definition

apply to all platforms. Although not nice, this should not affect other platforms, as nil should not be be defined using #define on any platform.

Compilation on apple gcc 32 bit platform now succeeds.

Disable test with high recursion depth, since it takes a long time

Allow skipping of long part of linearization_test1.

This one times out (>30minutes)

Guarded #undef nil by an ifdef suggested by Jeroen which is recognized properly by a 32bit mac with gcc.

Added computation of the control flow graph, using a reachability algorithm.

Attempt to fix build on Mac

Conflicts:

libraries/data/include/mcrl2/data/standard_utility.h

Some cleanup of code generator for standard data types

Conflicts:

libraries/data/build/data.py

Rename sort_list::nil to sort_list::empty.

This avoids the need of ugly workarounds on Mac, and is more in line with the naming conventions in sets and bags.

Conflicts:

libraries/data/include/mcrl2/data/detail/prover/induction.h
libraries/data/include/mcrl2/data/list.h
libraries/data/include/mcrl2/data/standard_utility.h

Fix a large number of obvious bugs on error paths.

Caught using the static analyser of Clang (scan-build). (Clang 3.1)

Conflicts:

libraries/aterm/source/hash.cpp
libraries/aterm/source/memory.cpp
libraries/aterm/source/safio.cpp
libraries/atermpp/source/bafio.cpp

Fixed clang compilation.

Do not use X server when generating help messages, man pages or XML data.

(Diagraphica-qt) Updated CMakeLists for Qt components, started cleanup of simulator.

Moved ltsview-qt settings infrastructure to qt-utilities.

(Diagraphica-qt) Partial cleanup of simulator.

Attempt to fix test failures in lts_lps2lts*_test.

It seems that we are running into race conditions, because both tests generate files with the same name, with the same timestamp. Try to avoid this by using a random suffix instead of a timestamp suffix.

Enable block test, if long tests should be enabled

Deprecate grapemcrl2

(Diagraphica-qt) Converted WX mouse and keyboard events to Qt events.

(Diagraphica-qt) Fixed visutils bugs.

Applied a patch from Gijs Kant to the ppg rewriter
Applied a patch from Gijs Kant to pbes explorer

Conflicts:

libraries/pbes/include/mcrl2/pbes/pbes_explorer.h
libraries/pbes/include/mcrl2/pbes/pbes_functions.h
libraries/pbes/source/pbes_explorer.cpp

Added pp overloads for std::set and std::list

Conflicts:

libraries/core/include/mcrl2/core/print.h

Implemented the Par function of lps2pbes using the traverser framework.
Implemented the Sat function of lps2pbes using the traverser framework.

Fixes #991.

Apply normalization of the state formula beforehand in lps2pbes. This is essentially what happens inside lps2pbes anyway. Used this to remove the negation part of the RHS function.
Rewrote state_formulas::normalize, to make it more readable.

Conflicts:

libraries/lps/include/mcrl2/modal_formula/state_formula_normalize.h
libraries/pbes/include/mcrl2/pbes/pbes_translate.h

Fixed standalone header compilation

Diagraphica-qt: wrote ltsview-qt-style settings system.

Implemented the RHS function of lps2pbes using the traverser framework. The timed and untimed versions have been merged. A check has been added to compare the output of the old and new RHS functions (protected with the flag MCRL2_DEBUG_RHS).
Removed some debug comments.

Conflicts:

libraries/pbes/include/mcrl2/pbes/pbes_translate.h

Prevent the empty domain optimization for quantifiers when the list of finite quantifier variables is not empty. This fixes ticket #1040.
Forgot to commit some files.
Removed old versions of files.
Added most recent versions of lps2pbes implementation.
Implemented the E function using the traverser framework, and merged the timed and untimed version (not completely finished yet).

Conflicts:

libraries/pbes/include/mcrl2/pbes/detail/pbes_translate_impl.h

Diagraphica-qt: lots of minor cleanup and WX removal.

Finished the new implementation of the E function in lps2pbes.
Removed old versions of E and RHS functions in lps2pbes, after verifying that the new versions produce the same outputs in all tests.

Conflicts:

libraries/pbes/include/mcrl2/pbes/pbes_translate.h

Converted lts2pbes to the traverser framework. Verified that the resulting pbesses for all formulae in the examples/abp directory are identical to the ones produced by the old version.

Conflicts:

libraries/pbes/include/mcrl2/pbes/lts2pbes.h

Fix build

Merged the untimed and timed versions of the lps2pbes algorithm.

Conflicts:

libraries/pbes/include/mcrl2/pbes/pbes_translate.h

Moved code from pbes_translate.h to lps2pbes.h

Conflicts:

libraries/pbes/include/mcrl2/pbes/pbes_translate.h

Updated the documentation of lps2pbes.
Improved the performance of must and may formulas.

Conflicts:

libraries/pbes/include/mcrl2/pbes/detail/lps2pbes_rhs.h

Added an entry for lps::state in the template overloads generation script, since the code for lps::state was added manually to generated code.
Added a section with some information about code generation scripts in mCRL2.
Improved the help text.
Added random process generator.
Added a random test for alphabet reduction.
Added a random test for lps2pbes. It checks for deadlocks on a random process both with lps2pbes/pbes2bool and lps2lts.
Make sure that an empty allow set gets printed (which is permitted according to the syntax).
Made preparations for testing the new alphabet reduction.
Adapted the mCRL2 syntax of sort expressions according to a suggestion of Ali Afroozeh. This solves an ambiguity in sort expressions in a much cleaner way than before.

Conflicts:

libraries/core/build/generate_parser_code.py

Add IEEE 11073-20601 session setup case study.

The case study is described in J.J.A. Keiren and M. D. Klabbers, "Modelling and verifying the IEEE Std 11073-20601 session setup using mCRL2", to appear in AVOCS 2012.

Use boost unit test instead of the minimal test facility.

If the unit tests are used with BOOST_AUTO_TEST_CASE, then setting: export BOOST_TEST_LOG_LEVEL="test_suite" before running a test will produce output like: Entering test suit "Master Test Suite" (...) Entering test case "test_simplify" (...) Leaving test case "test_simplify"; testing time: 20ms (...) Leaving test suite "Master Test Suite"

This way it is much more clear what test case is being executed/failing if the debug output is inspected.

Conflicts:

libraries/pbes/test/control_flow_test.cpp

(Diagraphica-qt) Fixed windows compile errors and warnings.

(Diagraphica-qt) Fixed event handler bugs.

Diagraphica-qt: made the opengl components toolkit-independent.

Diagraphica-qt: transformed opengl components into qt widgets; started work on the new main GUI.

(Diagraphica-qt) Fixed mouse events of ArcDiagram and fixed a minor bug in Bundle. Fixed painting of Visualizer objects.

(Diagraphica-qt) Started transformation of Parser.

(Diagraphica-qt) Improved Parser::parseFile.

(Diagraphica-qt) Fixed and improved MainWindow as far as needed to implement and test Parser.

(Diagraphica-qt) Transformed Parser (parseDiagram and parseShape).

Changed 'Cancel' case to default case to avoid very verbose GCC warning.

Added ctest-to-junit.xsl to support distributed Jenkins build.

Adding cross-platform build driver for Jenkins.

Typo.

Make script more verbose.

Just use first line of TAG file.

Try and make this work for windows

Not quite used to CMake yet...

Disable two tests that belong to bug #1019 (which was closed as wontfix)

Fix a few documentation bugs

Fix instructions for building boost

For the time being do not build the gui tools on windows

Provide CMake with absolute path to compiler.

Flush stdout after print.

Import sys...

Fixed rewriting of initial state in the next state generator.

Fixes #1043

Conflicts:

libraries/lps/include/mcrl2/lps/next_state_generator.h
libraries/lps/source/next_state_generator.cpp

Improve readability.

Add exact multi-action matching to lps2lts, experimental 'status'-level logging.

Conflicts:

libraries/lts/include/mcrl2/lts/detail/exploration.h
libraries/lts/include/mcrl2/lts/detail/lts_generation_options.h
libraries/lts/source/exploration.cpp
tools/lps2lts/lps2lts.cpp

(Diagraphica-qt) Updated parseShape with DOF. Implemented parseAttrConfig and parseAttribute.

(Diagraphica-qt) Replaced null by 0 in all files.

Make Maintainer-build cross-platform.

Diagraphica-qt: started implementing main window functionality.

Trying to make CMake scripts cross-platform and more readable.

Do not overwrite CXX_FLAGS from build script, do not use CMake cache.

(Diagraphica-qt) Finished Parser.

Add include for MSVC compiler (otherwise it picks the std::isalnum from the header).

Diagraphica-qt: removed wxWidgets dependencies; enabled diagraphica-qt in main makefile.

Diagraphica-qt: fixed a build issue.

Diagraphica-qt: Fixed openGL linking.

Diagraphica-qt: reduced mediator dependencies.

Diagraphica-qt: implemented plots.

Removed DARWIN compiler directives

(Diagraphica-qt) Fixed various bugs and implemented MovableTableWidget.

(Diagraphica-qt) Fixed column resizing of MovableTableWidget.

Diagraphica-qt: Fixed a build issue.

(Diagraphica-qt) Improved MovableTableWidget.

(Diagraphica-qt) Started transformation of DiagramEditor.

Allow semicolon at the end of an 'absfunc' declaration. Related to ticket #1045.
Updated the documentation of pbesabsinthe. Related to ticket #1045.

(Diagraphica-qt) Fixed DiagramEditor.

Diagraphica-qt: implemented cluster routing.

Diagraphica: implemented cluster hovering.

(Diagraphica-qt) Fixed various bugs in DiagramEditor.

Diagraphica-qt: implemented simulator and examiner clear operations.

Fixes #1049

Diagraphica-qt: Implemented arc diagram markings for examiner.

Diagraphica-qt: implemented arc diagram markings.

Diagraphica-qt: implemented the last remaining analysis-view component interactions.

Fixed the performance of specifications of the form c -> P + c -> P + ..., by using unary_op_right instead of unary_right. This fixes trac issue #1041.

Speed up PBES generation by +/- 16%.

Conflicts:

libraries/atermpp/include/mcrl2/atermpp/algorithm.h
libraries/atermpp/include/mcrl2/atermpp/detail/algorithm_impl.h

Diagraphica-qt: implemented clustering.

(Diagraphica-qt) Added itemMoved signal in MovableTableWidget.

Add example to the pbes control flow test in which no CFPs should be found

Revert workaround added in r10534.

The problem addressed by the workaround has been fixed properly in r10887.

(Diagraphica-qt) Transforming DiagramEditor (started with DofDialog). Minor fix in Shape. Removed useless Mediator in DiagramEditor.

Diagraphica-qt: implemented graph manipulation.

(Diagraphica-qt) Major clean-up of DOF, Shape and Diagram in order to better understand and fix all problems of DiagramEditor.

(Diagraphica-qt) Minor update of DOF.

(Diagraphica-qt) Partial transformation of DiagramEditor.

(Diagraphica-qt) Fixed creation of shapes.

Diagraphica-qt: fixed arcdiagram context menu drag and drop handling.

Diagraphica-qt: fixed trace view rendering.

Diagraphica-qt: minor cleanup.

Diagraphica-qt: implemented colorchooser and merged it with opacitychooser. Still buggy.

(Diagraphica-qt) Fixed various bugs mainly in DiagramEditor (shape creation, selection and copy/pasting).

Addresses compiler warning (set but unused variable)

(Diagraphica-qt) Fixed dragging of shapes.

(Diagraphica-qt) Fixed shape configuration in DiagramEditor.

Diagraphica-qt: fixed colorchooser.

Diagraphica-qt: fixed plot mouseover handling.

Diagraphica-qt: fixed trace view scrolling.

Diagraphica-qt: fixed simulator.

Fix build

Fix Mac build.

Fixed compiler warnings.
Fixed compilation error.

(Diagraphica-qt) Fixed: Keyboard shortcuts of DiagramEditor, size hints for various widgets, focus and drag of ColorChooser.

(mCRL2-gui-qt) Implemented requested features. Fixes #1036, #1037, #1038.

Improved LogWidget.

(mCRL2xi-qt) Improved error reporting of Parser, Rewriter and Solver which fixes #1047. Implemented save feedback which fixes #1051.

Conflicts:

tools/mcrl2xi-qt/parsing.h
tools/mcrl2xi-qt/rewriter.cpp
tools/mcrl2xi-qt/solver.cpp

Always use the new implementation of the nextstate generator in lps2lts.

Note: this removes the --alternative flag from lps2lts.

Install tool catalog to proper share directory.

Fixes #1004

Update performance measurements to the change in r10918

Implemented the 'structured' variant of lps2pbes, as defined by Gijs Kant.

Conflicts:

libraries/pbes/include/mcrl2/pbes/lps2pbes.h

Fix the commit from r10920 in case MCRL2_STAGE_ROOTDIR is not set.

Fix by jkeiren

Added an initial version of complps2pbes. It currently only checks if the process equations are linear, and if the initial state is in communicating LPE format.

Add package script for Jenkins

Factor out utilities from build.py into util.py
Add file that packages with CPack, depending on platform.

(mCRL2xi-qt) Implemented requested line numbering which fixes #1050.

Remove stray line from package script

Added icon
Initial focus set to texteditor.

Modify jenkins build to use out of source builds

Make the jenkins out of source build more robust

Fix installation of the tool catalog in the case that staging is not used

Use the out of source build setup for packaging as well

Add Jenkins script for generating documation (homepage)

Fix typo in documentation script

Remove SVN $Id$ directives from SVC library. This confuses the Jenkins build.

Conflicts:

3rd-party/svc/source/blocklist.cpp
3rd-party/svc/source/compress.cpp
3rd-party/svc/source/hashtable.cpp
3rd-party/svc/source/huffman.cpp

(Diagraphica-qt) Fixed run-time icon. (LTSGraph-qt) Fixed menubar location which fixes #1059. (mCRL2xi-qt) Fixed same menubar problem.

Extend changelog

Added version information to "About"-dialog for Qt tools.

(utilities_qt) Added ExtendedTabWidget and NumberedTextEdit. (mCRL2-gui-qt) Minor fix. (mCRL2xi-qt) Clean-up of DocumentManager and DocumentWidget. Used ExtendedTabWidget for DocumentManager which fixes #1056, #1057.

(mCRL2-gui-qt) Fixed reset perspective. (mCRL2xi-qt) Fixed build error. (Merged incorrectly.)

(Qt tools) Implemented saving and restoring of window geometry and state. Fixes #1061, #1062, #1063, #1064, #1065, #1066.

(LTSGraph-qt) Fixed INFILE loading and implemented label coloring which fixes #652.

(Qt tools) Checked all CMakeLists, fixed all icons, removed old diagraphica code and files, reverted unwanted replace, fixed all ui variables. Implemented PersistentFileDialog as utility which fixed #1067.

Conflicts:

tools/lpsxsim-qt/CMakeLists.txt

Extend package script to generate source package

Add missing )

Fix compiler warning about use of uninitialised value. The code was correct as it was, but it is probably nicer to initialise this anyway.

Set proper name for the binary packages

Simplifying/restructuring CMake, removing Wx tools from build.

Removing unused parser and lexer.

Conflicts:

libraries/core/source/mcrl2lexer.ll
libraries/core/source/mcrl2parser.yy

Fixed tool-catalog en tool detection on OS-X for mcrl2-gui-qt

Applied a patch for PBES explorer from Gijs Kant. It solves an infinite recursion problem, and it skips some unused equations when generating transition groups.

Conflicts:

libraries/pbes/include/mcrl2/pbes/pbes_explorer.h
libraries/pbes/source/pbes_explorer.cpp

Fix build

Apply the 'structured' parameter in the string version of lps2pbes (it was ignored).

Diagraphica-qt: implemented attribute configuration and diagram load and save. This finishes the diagraphica port.

The --action flag was broken. We need a test for this.

Dangerous commit, removing all WxWidgets code and still restructuring CMake. Apologies for any inconvenience.

Conflicts:

tools/diagraphica/CMakeLists.txt
tools/grapemcrl2/CMakeLists.txt
tools/grapemcrl2/libgrape/label.cpp
tools/grapemcrl2/mcrl2gen/mcrl2gen_validate.cpp
tools/grapemcrl2/mcrl2gen/mcrl2gen_validate.h
tools/lpsxsim/CMakeLists.txt
tools/lpsxsim/lpsxsimmain.cpp
tools/lpsxsim/lpsxsimmain.h
tools/lpsxsim/lpsxsimtrace.cpp
tools/lpsxsim/lpsxsimtrace.h
tools/lpsxsim/plugins/trace/xsimtracedll.cpp
tools/lpsxsim/plugins/trace/xsimtracedll.h
tools/ltsgraph/CMakeLists.txt
tools/ltsview/CMakeLists.txt
tools/ltsview/markstateruledialog.h
tools/mcrl2xi/CMakeLists.txt
tools/mcrl2xi/gui/actions.cpp

SVN did not apply these deletions in previous commit.

Forgot to include libraries/utilities/CMakeLists.txt

Remove the old nextstate generator, simulator and state space exploration code.

This has been superseeded by the implementation by Ruud Koolen.

Conflicts:

libraries/lps/include/mcrl2/lps/next_state_generator_old.h
libraries/lps/include/mcrl2/lps/nextstate/standard.h
libraries/lps/include/mcrl2/lps/simbase.h
libraries/lps/include/mcrl2/lps/simulator.h
libraries/lps/source/nextstate_standard.cpp
libraries/lps/source/simulator.cpp
libraries/lps/test/nextstate_test.cpp
libraries/lps/test/symbolic_reachability_test.cpp
libraries/lts/include/mcrl2/lts/detail/exploration_old.h
libraries/lts/include/mcrl2/lts/detail/lps2lts_lts.h
libraries/lts/include/mcrl2/lts/detail/queue_old.h
libraries/lts/source/exploration_old.cpp
libraries/lts/source/lps2lts_lts.cpp

Add the documentation of the new nextstate exploration strategy.

Document courtesy of Ruud Koolen. This is his report for the FSA seminar (2IF96), 2011/2012.

Fixes for Mac OSX.

Fixed Clang identification. Removed '-pthread' option for GNU compilers (we'll put it back if it turns out to be essential).

Conflicts:

libraries/atermpp/include/mcrl2/atermpp/algorithm.h
libraries/atermpp/include/mcrl2/atermpp/detail/algorithm_impl.h
libraries/atermpp/test/algorithm_test.cpp
libraries/atermpp/test/replace_test.cpp
libraries/data/source/detail/enumerate/enum_standard.cpp

Reverting last commit, committed too much.

Conflicts: libraries/data/source/detail/enumerate/enum_standard.cpp

Fixed Clang identification. Removed '-pthread' option for GNU compilers (we'll put it back if it turns out to be essential).

Workaround for windows pathname limits.

On Windows, a path can be a maximum of 256 characters. Due to the structure of the Jenkins paths, we outrun this limit when generating a package. As a workaround, we generate the package to C:\Temp\pkg.

Forgot to remove -Wl,-as-needed flag from plain C compiler.

Move the graphical tools from their -qt directories to the normal directories.

Ported symbolic link exporting tool to Qt.

Improve nightly build.

Add script to clean up the build directory (currently used for the nightly build)
Fix links to binary packages on the generated homepage.
Adapted the computation of control flow parameters, after discussion with Jeroen.

Fix stupid mistake in download link (.exe -> .rpm)

Removed irrelevant Boost components. Boost system is the only one left. It is only required for ctest targets.

Fixed installation of OSX bundles created with Qt's MacPort. Bundles fixups are now processed via Cmake's "BundleUtilities" script. Fix for other Qt installations will follow.

Conflicts: libraries/bes/test/boolean_expression_test.cpp libraries/pbes/test/pbes_test.cpp

Split up the code of the control flow algorithm.
Implemented marking algorithm (not completely finished yet!).

Fixed Bundle installation when using official QtSDK.

Removed superfluous linking to Boost libraries.

Conflicts: libraries/utilities/include/mcrl2/utilities/test_utilities.h

Finished marking algorithm, and added logging.
Fixed \file attribute of sorted_sequence_algorithm.h.

Fixed mcrl2 build.

Conflicts: libraries/bes/include/mcrl2/bes/boolean_equation_system.h

Fix a number of compiler warnings.

Related to bug #917

Remove wxwidgets references from documentation.

I also started build instructions with wxWidgets for Windows and Linux; can the ones with relevant experience please include the instructions for MacOSX?

Remove unused documentation file

Build GUI tools on windows in Jenkins

Extend QT windows instructions

Fixed computation of the control flow graph. If a guard evaluates to false the corresponding edge is skipped.
Improved logging.
Fixed computation of initial marking.
Completed the implementation of the marking algorithm. N.B. It needs further testing.

(mCRL2-gui) Implemented requested features. Fixed reported bugs. Removed GrapemCRL2 from the catalog. Changed isGui string argument of ToolInformation to public boolean.

(mCRL2xi) Fixed view actions for panels.

(Qt tools) Removed unused QDebug includes.

(LTSGraph) Implemented requested features. Panning is still not optimal but I can't locate the exact cause.

(LTSGraph) Fixed commit.

Change RelocateInstallTree to include Qt dynamic libraries on Windows.

Warning: this still needs proper testing on all platforms, sorry for any inconvenience!

Attempt to fix RelocateInstallTree

(Qt tools) Minor improvements.

Another attempt at fixing install tree relocation

Added more descriptive parse errors. Addresses #873.

Fix detection of Qt libraries on Windows. This should fix packaging with dynamic Qt libraries on Windows

Remove accidentally added line of code

Check if directory exists, before we remove it

(DiaGraphica) Fixed all DiagramEditor problems (transformations and rotations). Fixed #449 (text rendering).

Fix build

Fix usage of std::isalpha, introduced in r10994

Update the instructions for Qt on Windows as I've used them for the build farm.

Fix (hopefully), MacOSX single bundle build

Consistently install all tools with the Runtime component.

Note: this was needed for the graphical tools; and will enable more modular packages in the future

Made the || and && operators left associative again.
Enabled warnings for expressions that are parsed differently.

This is related to ticket 919, and the commits 10022 / 10046. It needs to be checked whether this change affects the performance of the parser. It turns out that parsing all specifications in the example directory is actually faster after this change (10 seconds versus 12 seconds).

Fix components for libraries, headers and examples

This fixes #981

Conflicts: libraries/aterm/CMakeLists.txt

Attempt to improve the look and feel of the Windows installer

(DiaGraphica) Minor fix.

Changed the location of the tool catalog such that it can be found by mcrl2-gui.

Clean up and restructure the packaging script

Reverted commit 11005. At the meeting is was decided to postpone this until after the release.
Fixed unused variable warnings.
Added a pbes rewriter that replaces outer level data operators by their pbes equivalents. The operators are !, ||, &&, =>, forall, exists.

For example val(b && c) is replaced by b && c.

Extended the one point rule rewriter.
Apply the data2pbes rewriter as a preprocessing step to the one point rule rewriter, to get rid of the mixed data and pbes operators.

Do not fix bundles on Linux.

(DiaGraphica) Improved DOF editing code of DiagramEditor.

Add remark that MS KB2280741 fix needs to be installed for MSVC.

On 64-bit Windows, building a release version of Qt (tested for 4.8.2), we run into the bug described at https://bugreports.qt-project.org/browse/QTBUG-17899. Installing the hotfix described at http://support.microsoft.com/kb/2280741 fixes this problem with the /O2 optimisations.

Use destdir in packaging; hopefully this fixes packaging on Ubuntu

One more step toward working package generation

Simplify globbing for header files.

Conflicts: libraries/aterm/CMakeLists.txt

Remove tool specific logger from pbespgsolve

This is in line with what has been discussed yesterday.

Add tool catalog to Applications component on non-apple platforms

Diagraphica: fixed two minor bugs.

LpsXSim: enabled tau prioritization.

LpsXSim: Implemented experimental dockable log widget.

LpsXSim: Made the dockable log widget expand at the first log message.

LtsView: Changed tool selection to use modifier keys instead of menu options.

LtsView: Fixed zooming-related crash.

LtsView: Fixed item selection bug during simulation.

Added an option to lps2pbes to use 'unoptimized' boolean operators. I.e. expressions like (true && x) are not simplified. This completes ticket 987.

Conflicts: libraries/pbes/include/mcrl2/pbes/detail/lps2pbes_e.h libraries/pbes/include/mcrl2/pbes/detail/lps2pbes_rhs.h

Added an option to txt2pbes to normalize the result. The default value for this option is true. At some point this should be reversed.
Implemented resetting of variables.
Added pbesstategraph tool.
Disabled the empty domain optimization in forall/exists. It turns out that in lps2pbes this optimization may not be used. Noted by Gijs Kant, while also the random tests were failing because of this.
Added random test for the structured option of lps2pbes.
Forgot to commit pbesstategraph directory in an earlier commit.
Moved the conversion to PFNF normal form to another place. This was done to ensure that the input of pbesstategraph is always in the expected form.
Added a test for the PFNF rewriter

LtsXSim: Fixed a crash bug during rapid simulation.

LtsView: changed info dialog, mark dialog, simulation dialog, and part of the settings dialog into docks.

LtsView: disabled zoom commands when unavailable.

LtsView: moved LTS loading and restructuring into a worker thread.

Fixed tau confluence support in simulation library.

LpsXSim: fixed a crash bug when random-playing through a deadlock state.

LpsXSim: disabled play buttons at appropriate times.

LpsXSim: implemented standard log dock.

LpsSim and LpsXSim now use the proper rewrite strategy.

Fixes #1046

Fix build

Added random test for pbesstategraph
Fixed a bug in reset_variables (the order of two statemens was wrong)
Added two failing 'random' test cases to control_flow_test.cpp. They trigger an assertion failure in pbes2bool.
Fixed an unused variable warning
Fixed two failing pbesstategraph test cases, found by random testing
Added missing include to pfnf_pbes.h
Added two new failing test cases, found by random testing.
[release]? Fixed resolve_name_clashes function.
Added some print statements. It is unknown why a test case fails in the context of control_flow_test.cpp, but succeeds when run from the command line.

Somebody set the data_expression to be returned to its default value, and then printed it. This led to a @novalue being printed in error messages.

This resolves #1052

Should be included in the release.

Added missing include
Added protection against garbage collection
Temporarily disabled two tests
pfnf_pbes no longer keeps a reference the original PBES

Conflicts: libraries/pbes/include/mcrl2/pbes/detail/control_flow.h libraries/pbes/include/mcrl2/pbes/detail/pfnf_pbes.h

Fixed typo in Ubuntu download link on the nightly build page.

Resolves bug #1024.

A .aut file with non consecutive state numbers is now read. This means that a file written using bit hashing can now be read.

The rational test has been adapted. The ltsconvert tests should not be run, because lps2lts does not work. This does not work with -rjittyp. As lps2lts does not work not .aut, .fsm and .lts files are generated. This means ltsinfo, ltsconvert and the ltscompare tests can not be run. For reasons that I do not understand the ltscompare tests are still running on my machine.

Conflicts: scripts/MCRL2TestTargets.cmake

I left two residual errors, one due to me in the previous commit.

When reading a .aut file the initial state and the value 0 were mixed up in the translation table.

When writing a .aut file generated using bit hashing, the initial state was set to 0, instead of to the bit hashed valued. This led to a transition system with one state too many, and unreachable transitions.

Apply the simplifying rewriter as a post processing step to the one point rule rewriter (requested by Tim).
Implemented the computation of control flow parameters using a fixpoint computation. This solves all known problems. However, the random tests have revealed another problem case.

Conflicts: libraries/pbes/include/mcrl2/pbes/detail/control_flow.h

Somebody wrote .bcg} whereas he meant .bcg in the test targets, leading to confusion and failing tests.

Should be included in the release.

Added to_string member function to sequence_sequence_substitution (should have been part of earlier commit)
Fixed the computation of the initial marking. When there are no implications in the right hand side of a PFNF equation, the function h is now considered as a guard.
Added a test case for this.

Now a complete run of random tests for pbesstategraph has succeeded.

Conflicts: libraries/pbes/include/mcrl2/pbes/detail/control_flow.h

Fixed the year in copyright note.

Removed superfluous file, spotted by Wieger.

Updated symbolic_exploration to the new specification.
Added a random test for symbolic_exploration.

Replaced lpsconvert (which does not exist....) into ltsconvert. This should be included in the release.

Adapted the use of MCRL2_SYSTEM_SPECIFIC_ALLOCA in a loop, by replacing it by a static vector, in an attempt to reduce excessive stack usage.

The following files use MCRL2_SYSTEM_SPECIFIC_ALLOCA within a loop, still.

libraries/data/source/detail/rewrite/jitty.cpp libraries/data/source/detail/rewrite/jittyc.cpp libraries/lps/source/next_state_generator.cpp libraries/pbes/include/mcrl2/pbes/pbes_explorer.h libraries/pbes/test/pbes_explorer_test.cpp

Conflicts: libraries/data/source/detail/enumerate/enum_standard.cpp

Added options to symbolic exploration to generate clustered and/or optimized results.
Extended the random tests to try all combinations of options.
Added extensive debug output.

Conflicts: libraries/pbes/include/mcrl2/pbes/detail/symbolic_exploration.h

Fixed a typo in symbolic_exploration that caused the clustered variant to be ignored.
Postponed the addition of generated cluster equations to the end, to avoid invalidation of iterators.

Add boost-test library to boost installation instructions

In Jenkins, run the full tests if we are building the release branch

Made some changes to the algorithm after discussion with Tom.

Avoid an expensive check for simple expressions.
Introduce clusters at the right places.
Maintain a sequence of bound variables.
Applied one more change that was discussed with Tom. The random tests for GBQNF normalization now succeed with all 4 variants.

[release] Fix a bunch of CLang compiler warnings

Use "throw parser.error(msg)" rather than "parser.error(msg)" to avoid warnings (previous implementation obfuscates control flow)
Parser now throws mcrl2::parse_errors.

Made explicit which for_each and find_if are used (the std:: or the atermpp:: implementation)

[release] Make compiled rewriter robust against compile script path with spaces.

[release] Fail if CADP support was requested but not honoured. Previously, this would only give you a warning.

Code readability.

Compared the use of MCRL2_SYSTEM_SPECIFIC_ALLOCA versus static and non static use of vector in the loop in the enumerator. Results are somewhat unexpected. I used state space generation of 1394-fin.

MCRL2_SYSTEM_SPECIFIC_ALLOCA: 36.2s static vector 37.4s vector 36.3s

As a vector does not overflow the stack I left the stack in place.

I did not adapt the ugly pointer argument in ApplyArray, because this requires to rewrite the old ATerm library to contain iterators. These are present and used in the new merged atermpp library.

Conflicts: libraries/data/source/detail/enumerate/enum_standard.cpp

Adapted the use of MCRL2_SYSTEM_SPECIFIC_ALLOCA within loops. In next_state_generator.cpp they have been replaced by vectors, with no measurable influence on performance on 1394-fin.

In pbes_explorer MCRL2_SYSTEM_SPECIFIC_ALLOCA could simply be moved out of the loop.

The only file that still uses MCRL2_SYSTEM_SPECIFIC_ALLOCA within loops is libraries/data/source/detail/rewrite/jitty.cpp.

Conflicts: libraries/lps/source/next_state_generator.cpp libraries/pbes/include/mcrl2/pbes/pbes_explorer.h

Adapted the worst occurrence of MCRL2_SYSTEM_SPECIFIC_ALLOCA in a loop in the jitty rewriter. All other occurrences do not seem to be too problematic. This should reduce excessive usage of the stack while applying jittyc rewriting.

Performance tests on 1394 show no notable difference in performance.

With this commit, I consider adapting MCRL2_SYSTEM_SPECIFIC_ALLOCA in loops as done.

Conflicts: libraries/data/include/mcrl2/data/detail/rewrite/jitty.h libraries/data/source/detail/rewrite/jitty.cpp

Generate new clusters at two more places.

LtsView: Fixed some spurious compiler warnings.

Merge test change from release branch

Change test for divide2_500 into divide2_100 in order to increase performance.

Merge 11110, 11111, 11112 from release branch.

Print some info about the variables passed into the build script

More robust detection of the build of the release branch

Modify detection to properly look at the jobname.

Jobname includes all details, which is why this detection did not work properly previously.

[release] Improve performance of ltsmin interface.

In state space exploration in mCRL2, we make sure that data equations that will definitely not be used when generating the state space are remored, prior to generating the rewrite system. Experimence has shown that this can lead do dramatic performance gains. In the LTSmin interface, it turns out that this was omitted so far. Enabling the used equation selector in said interface also gives a performance gain here.

Before: lps2lts-seq 1394-fin.lps real 3m21.881s user 3m19.460s sys 0m2.012s

After: lps2lts-seq 1394-fin.lps real 1m34.264s user 1m33.766s sys 0m0.388s

Remove the template parameter for the identifier generator of data_enumerator. This simplifies the construction of quantifier elimination rewriters.
Added a constructor to enumerate_quantifiers_rewriter.

Conflicts: libraries/data/test/enumerator_test.cpp

Added is_guarded predicate for process expressions.

Conflicts: libraries/process/test/process_test.cpp

Added 'symbolic exploration' variant of pbesinst. This variant can be used to compute a structure graph.
Added an option to instantiate the PBES in the symbolic_exploration tool.

Conflicts: libraries/pbes/test/pbesinst_test.cpp

Improved printing of disallowed multi-actions in an allow operator.

Another improved to printing disallowed multi-actions in an allow operator.

Fix nextstate generator check on conditions.

The new implementation of the nextstate generator failed to check whether the solutions provided by the nextstate generator are exact. This means that the nextstate generator would enable transitions with non-false guards, instead of transitions for which the guard was true.

Now if the solution is not exact, we fail with an mcrl2::runtime_error.

Fixes #1073 of which #1075 was a duplicate.

Fix check for mCRL2-release in Jenkins build.

This should fix the running of all >7000 test cases in the continuous build.

Spotted by Sjoerd.

Added linking to aterm library for resolving lazy symbol binding failure: Symbol not found: __ZN5aterm11ATmakeAppl5EmPNS_6_ATermES1_S1_S1S1

Failure occurs on OS-X 10.6 on with "pipes.mcl2" example. Example is available upon request.

Proper fix for compiling rewriters.

This is an improvement over the fix in r11124, that in addition cleans up the configuration of the compiling rewriter dramatically.

[release] Improve the error message introduced in r11122.

[release] Call the parents keyPressEvent method in the FileBrowser.

This fixes an infinite recursion of FileBrowser::keyPressEvent calling itself, leading to crashes when creating/renaming new files/directories.

Fixes #1076

Clean out some #if 0'd code

Fix a number of compiler warnings.

Related to #917

Attempt to fix #1079.

It seems that on some compilers the following pattern does not work.

class A { public: class B { friend A;

private: bool m; };

class C { protected: bool x;

public: C(B b):x(b.m) {} }; };

In other words, friend A does not imply friend A::C.

Fix the documentation of div and mod (they are infix, not prefix).

This issue was spotted by Jaco van de Pol; I also added a language example in which all operators on numbers are exercised.

[release] Improve the error message if condition does not rewrite.

Per JFGs request, improve the error message in the next state generator to include the valuation in the substitution when rewriting condition; furthermore, do not print the complete condition, instead we just give a hint, by printing the first 80 characters of the condition.

Related to bug #1073.

[release] Remove extremely long running test case.

The remaining test case in linearization_test1 was added to linearization_test. This at least ensures that we can run the linearization test within the 1500 second time limit

Clean up test for ltscompare.

Conflicts: libraries/lts/test/trace_compare.cpp

Add test case for bug #1082

Treat function symbol for trace_pair in standard way.

The handling of trace_pairs, which was done all manually, lead to crashes. We now use the same mechanism of static initialisation that is used in other places as well.

Fix #1082

Conflicts: libraries/trace/include/mcrl2/trace/trace.h

Copy data specification in pbesstategraph

Adjust test case for lpsbinary to give more useful information.

This test is failing on 32bit linux in Release mode.

Conflicts: libraries/lps/test/binary_test.cpp

Add test case for bug #1085

Added proper handling of global variables to pbesstategraph.

[release] Fix linking problem with compiling rewriters on MacOSX.

The issue here is that the executables that we built were stripped, which rendered some of the symbols unavailable to the dynamic library created for the compiling rewriter.

Clearly documented in the CMake code that stripping should not be used on the Mac!

Fix together with jkeiren.

Remove WXMAC define from CMake scripts

Separated the computation of the source and destination function. The reason for this is that the source function is needed for the stategraph algorithm, while the destination function is not.

Fix build

Fixed #1085.

A list of action names was assigned to an identifier string, which was not accepted in debug mode (but would not have caused problems in release mode).

As the string was only used to add a postfix to names of newly introduced variables, and the names of the multi-actions were not at all used for this purpose, the erroneous assignment has been removed.

All self tests appear to succeed, including the new one indicating this problem.

Conflicts: libraries/lps/source/linearise.cpp

Set the initial state to 0 in the dot parser. This should fix issue #1083. The ticket will be closed if the Windows tests succeed.

Fix #1087

The floating point computation that was used to determine the number of Boolean variables needed to represent finite data types was inaccuratie on some platforms. Instead we now just compute the ceil(log2(n)) by looking at the leftmost bit of n that is true.

[release] Inline two functions in binary.h

Spotted by Wieger

Attempt to fix bundle creation on MacOSX.

This reintroduces the fix from r10359, which was inadvertedly removed in r10954. For creating bundles on MacOSX we need to ensure that the boost libraries and the header files have been packaged into the bundle, in order to build the compiling rewriters.

This needs testing.

Fix changeset in r11171

Typo

Added an option to pbesstategraph to apply reduction to the initial PBES instead of to the one in PFNF format.
Separated the reset variables computation from the control flow graph computation.

Conflicts: libraries/pbes/include/mcrl2/pbes/detail/control_flow.h

Streams writing to std::cerr are redirected to mCRL2 logger library

Removed obsolete file. Functionality is replaced by Qt.

Repaired an obvious error in jittyc, where due to a typing mistake the "or" case was not treated properly. This error may have been in the jittyc rewriter for years. It is not clear why it was not triggered earlier. It was found in the toolset based on the new aterm library, where it caused failing tests.

Updated the CMakeLists file for lpsrealelm, to allow printing of summands.

Conflicts: tools/lpsrealelm/CMakeLists.txt

Fixed a warning

Fixed installation of Boost headers for a single bundle application on MacOSX.
Added missing Boost headers.
Fixed compilerewriter script detection for a single bundle application.
Disabled linking to Boost libraries in compilerewriter script.

[release]

Conflicts: libraries/data/source/detail/rewrite/jittyc.cpp

Layout improvement of mCRL2-gui.

[release]

Made a test for the one point rule rewriter resistent against changes in the argument order of conjunctions and disjunctions.

Conflicts: libraries/pbes/test/rewriter_test.cpp

Fix protection issue in lts_lts_t

The process parameters and action labels should be protected, otherwise there is a risk of them being garbage collected.

This was caught using a test run with -DDO_AGGRESSIVE_GARBAGE_COLLECT

Conflicts: libraries/lts/source/liblts_lts.cpp

lpsrealelm added for all real variables r a condition r>=0 and for all real variables in a sum the condition r>0. This under the assumption that these variables represented times. With the example of Cinderella and her stepmother where the stepmother poors real valued amounts of water in buckets, these constraints do and should not apply, and therefore have been removed.

Conflicts: tools/lpsrealelm/realelm.h

[release] Properly document changeset r11180, and clean it up.

The change to jittyc.cpp that was made in r11180 could be done in a lot more readable way, by (re)using the file_exists function, that was implemented in uncompiledlibrary.h; I moved this to the more suitable file_utility.h.

Furthermore, this changeset adds clear documentation as to why these changes were implemented in this way (MacOSX), such that they are not likely to be removed inadvertedly in the future.

Add test cases that show that bug #1092 is invalid.

Make lps2pbes test more systematic, and clean up the test code

Conflicts: libraries/pbes/test/lps2pbes_test.cpp

Add test case for bug #1090

Add missing "

Implemented a fix for trac issue 1090. In both the Sat function and the E function identifier generators were used that were not initialized with identifiers appearing in the data specification of the LPS. This has been fixed by passing a properly intialized identifier generator as an additional argument to these functions.

Conflicts: libraries/pbes/include/mcrl2/pbes/detail/lps2pbes_e.h libraries/pbes/include/mcrl2/pbes/detail/lps2pbes_sat.h

Fixed compilation of lts2pbes, by adding an identifier generator argument to calls of the Sat function.

[release] Improve explanation in Gossip tutorial.

Based on remarks by Muck van Weerdenburg and Christian Krause on the mcrl2-users mailing list

Extend lps2pbes test with expected failing test case.

Add test case for bug #1094
Fixed trac issue 1094. Changed the order of name clash resolving and type checking in the parser for state formulas. This allows the type checker to catch unbound variable errors in state formulas.

Move test case for #1094 to state_formula teest; it is a parsing/typechecking issue.

Conflicts: libraries/lps/test/state_formula_test.cpp

Fix layout in package documentation

Bump version to 201210.0 and finish changelog.

Update download links

Made an algorithm class for invelm.
Improved the structure of the algorithm.
Removed all applications of of deprecated::summand.
Removed the option to select a summand index.

This new implementation of invelm can be applied after the release, and after some tests for invelm have been added.

Merge 11219 from release branch

Allow to build release packages through environment variables in Jenkins

Merge 11221 from release branch

Fix typo

Removed occurrences of deprecated::summand in untime.
Removed deprecated::summand from suminst and sumelm tests.

Conflicts: libraries/lps/test/suminst_test.cpp

Added missing copyright notice.

Conflicts: libraries/lps/test/symbolic_reachability_test.cpp

Removed usages of deprecated::summand from symbolic reachability test.
Removed a usage of the std::map::at function, since it is not properly supported on the Mac.
Added a test case to invelm_test that checks if the simplify_all and no_elimination options work as expected.

Adapted two PBES tests, which could not be compiled on a mac with OS10.5.8. Not for the release.

Removed usages of deprecated::summand from lpsinvelm.
Removed the option to specify a summand number from lpsinvelm.
Restructured the lpsinvelm code, to make the logic of the algorithm visible.

Conflicts: libraries/lps/include/mcrl2/lps/invariant_eliminator.h libraries/lps/source/invariant_eliminator.cpp tools/lpsinvelm/lpsinvelm.cpp

Fixes #1095

The problem is a missing declaration (ATermAppl) that is not properly generated in the compiling rewriter because a variable arity does not reflect the arity of the main function at some point. As a solution the cast (ATermAppl) is generated always at the appropriate point.

This fix must be incorporated in the release.

Conflicts: libraries/data/source/detail/rewrite/jittyc.cpp

Removed tool tests for lpsinvelm with the option -s, since it has been removed. Spotted by Jan Friso.
Replaced two occurrences of std::map::at by the workaround map_at, to make it compile on the Mac.

Removed deprecated summands from lpsrealelm.

Made a few protected functions protect and unprotect public, as these are required in lpsrealelm, and will be removed shortly anyhow.

Conflicts: libraries/lps/include/mcrl2/lps/deadlock.h libraries/lps/include/mcrl2/lps/multi_action.h libraries/lps/include/mcrl2/lps/summand.h tools/lpsrealelm/realelm.cpp tools/lpsrealelm/realelm.h

Removed usages of deprecated::summand.

Conflicts: tools/lpsparunfold/lpsparunfoldlib.cpp

Removed an obsolete typedef for deprecated summands.

Conflicts: tools/lpsparunfold/lpsparunfoldlib.h

Fix typos ("unkown" -> "unknown"), caught by Debian's Lintian tool

Merge 11247 from release branch

Fix download path for windows installers

Removed deprecated summands from the lineariser. All tests succeed. But the lineariser test in debug mode does not terminate within the time out. This suggests that linearisation did become a little slower.

This means that deprecated summands are not used anywhere and can be removed from the library.

Conflicts: libraries/lps/source/linearise.cpp

Fixed ambiguous reference to ‘log’, detected using GCC 4.2.1 (Darwin)

Fix build

Removed deprecated summands.

Conflicts: libraries/lps/include/mcrl2/lps/linear_process.h libraries/lps/include/mcrl2/lps/summand.h

Fixed standalone compilation.
Corrected the definition of is_guarded, such that the case P # Q, Qa.P is considered guarded.
Updated the implementation of is_guarded to the adapted definition.
Made an attempt to repair the definition of alphabet reduction with respect to process instances.

Added option that enables filepicker to open a file.

Fixes #1096

Conflicts: tools/mcrl2-gui/filepicker.cpp tools/mcrl2-gui/filepicker.h

Normalize the input of pbesstategraph.
Applied the logging library to pbesstategraph.

Conflicts: libraries/pbes/include/mcrl2/pbes/detail/control_flow_graph.h libraries/pbes/include/mcrl2/pbes/detail/control_flow_reset_variables.h

Added possibility for second input file for tools in mcrl2-gui.

Fixed typo in control flow test.
Made a number of corrections to the alphabet reduction algorithm, after discussion with Jan Friso.
Introduced an additional parameter W to the alphabet reduction function that stores process identifiers that were encountered before. This was needed to break an infinite recursion that occurred in equations like P = a.P.
Updated the documentation.
Fixed misspelling of the function txt2lps.
Added a test for replacing variables.
Suppressed some unused variable warnings.

An example made at the VU, which came to me by Tim Willemse, showed (a.o.) a very slow lineariser. One of the problems turned out to be that substitution of data terms was very slow becaused the new map based substitutions were mixed with old style list based substitutions. What happened was that just before substituting a variable the lists were transformed into a map, after which the substitution was carried out.

In the case of the specification TestAllThings.mcrl2 there is a very noticable difference in performance.

Conflicts: libraries/lps/source/linearise.cpp

Minor cleanup of the lineariser.

Conflicts: libraries/lps/source/linearise.cpp

Declare qreal instead of double.

Fixes #1100

Attempt to fix man page generation on OSX Lion.

This is an attempt to resolve bug #1099. (untested)

Fix some warnings in release mode

Conflicts: libraries/aterm/include/mcrl2/aterm/memory.h

Use the action specification to initialize the alphabet.
Removed some debug statements.
Added function find_action_labels to the LPS, PBES and process library.
Initialize the alphabet with action names that appear in the specification.
Added find_action_names function that takes names appearing in block, hide, ... into account.
Fixed find_action_labels (the results were not properly collected).
Fixed handling of atermpp::vector in the dependencies calculation of the traverser generation script.
Removed find_action_labels for PBES, as it makes no sense.
Improved debugging output of alphabet reduction.

Fix some spelling errors in docs.

Fix #1104 (dead compiling mCRL2 yourself link)

Fix #1105 (Wrong link to regression test results)

Fix some dead links in the documentation

Update changelog in trunk

Bump version to 201210.1

Properly set font of checkbox labels to bold in mcrl2-gui.

Fixes #1107, which was introduced in r11181.

Merge 11303 from release branch

Update changelog

Added a test for replace_free_variables
Improved code generation for pbes and boolean_equation_system

Conflicts: libraries/core/build/mcrl2_classes.py

Added a definition of the alphabet of a process expression. This is an extension of the definition given in the mCRL2 book.
Implemented a function that computes the alphabet of a process expression.
Adapted alphabet_traverser such that it can become a base class for alphabet reduction.
Added a test case for alphabet_traverser.

Allow the user to provide path to binaries to documentation generation script.

The -p/--path option to generate.py can contain the path to the mCRL2 binaries; by default the variable is empty, and the script simply searches for the tools in the $PATH.

The option is used in the make doc and make fastdoc targets. Fixes #1108.

Update changelog

Update download page

Fixed a bug in the simplify routine of pbesstategraph. Expressions were simplified, but the result was not assigned.
Fixed a typo in the simplify routine of pbesstategraph. This was not noticed before because the functionality was unused.
Simplified the specification of alphabet reduction, after discussion with Erik de Vink.

Prepared settings for creating a binary distribution on OS-X. This includes the following changes:

Tools are installed in a directory structure.
Updated mCRL2-gui icon (for OS-X).
Man pages are part of the installation "Documentation" component.
Alias for mcrl2-gui is created after installation.

Removed obsolete "macosx" folder

Changed MCRL2_SINGLE_BUNDLE into MCRL2_OSX_PACKAGE.

Use the propositional variable of the vertex instead of the edge for updating marked variables.
Fixed wrong answer in control flow test.
Cleaned up some using statements

Conflicts: libraries/lps/include/mcrl2/lps/multi_action.h

Made a new implementation of alphabet reduction (work in progress).
Introduced bounded_alphabet_traverser that computes the intersection of the alphabet with a given set of multi action names A.
Added functions for testing alphabet routines.
Added tests for alphabet operations.
Use multiset operations instead of set operations when dealing with multi action names.

Clean up some tests.

In the lps_linearization_test, it is completely unclear what the purpose of test_large_specification is. Since it causes timeouts I remove it.
The specification "block" in the same test is run in the performance measurements.

The flag MCRL2_SKIP_LONG_TESTS is now superfluous, as it should be.

I propose removing the flag from CMake as well.

Deprecate tbf2lps.

The ATerm formats are not compatible anymore.

Removed bounded_alphabet_traverser, since filtering intermediate results turned out to be more complicated than expected.
Added handling of the communication operator. Alphabet reduction of ABP now gives a bisimilar result.
Updated the documentation of alphabet reduction.

qreal != double on ARM, causing build failures. Attempt to fix.

Improved the simplify routine of pbesstategraph, by replacing data operators !, &&, || by their PBES equivalent in a preprocessing step. After this the data expression !(val(!(d !# v)) || val(!(s= 4))) is simplified successfully. Note that again the artificial distinction between logical operators of data expressions and pbes expressions is causing difficulties.
Added missing namespace qualifications.
Updated the specification of the push_allow operator.
Updated the implementation of apply_comm_inverse according to the corrected definition.
Added a test.
Added handling of the rename operator to push_allow.
Added tests for apply_comm, apply_rename and apply_rename_inverse.
Adapted apply_comm according to changes in the specification.
Added tests for comm/rename.
Applied boost unit test framework.
Added handling of block and allow, and corresponding tests.
Fixed the apply_comm function. It's definition has been changed to correctly handle terms like a(1) | b(2).
Improved debug output of push_allow.
Implemented several missing operators of push_allow.

Fixes #1112

Made several corrections to push_allow, as a result of testing with several larger examples.
Fixed left_arrow operator.
Fixed handling of pCRL expressions. It turned out that non-pCRL operators may occur in the scope of pCRL operators, which was not anticipated.
Improved debug output.

Fix build

Fix reading of aterms

Fix bug in next state generator.

If you use indices into a vector directly, you should use resize instead of reserve.

std::vector actions; actions.reserve(1); actions0;

will lead to segfaults and unpredictable behaviour

Fix a bunch of compile errors and warnings in tests

Fix failing tests

mCRL2org / mCRL2

Allow closing of multiple tabs in mcrl2xi #1059

2012-08-21 11:51:35: @jkeiren created the issue

2012-08-21 13:18:18: r.c.boudewijns@student.tue.nl changed status from new to accepted

2012-08-21 13:18:18: r.c.boudewijns@student.tue.nl changed owner from rboudewijns,fstapper to rboudewijns

2012-08-21 15:42:55: r.c.boudewijns@student.tue.nl changed status from accepted to closed

2012-08-21 15:42:55: r.c.boudewijns@student.tue.nl set resolution to fixed

2012-08-21 15:42:55: r.c.boudewijns@student.tue.nl commented

2012-11-13 07:51:16: @jkeiren commented