search

mCRL2org / mCRL2

The Git repository for the mCRL2 toolset.
https://mcrl2.org/
Boost Software License 1.0
88 stars 37 forks source link

lpssim/lpsxsim does not correctly handle global variables #1075

Closed jgroote closed 12 years ago

jgroote commented 12 years ago

Issue migrated from trac ticket # 1073

component: lpsxsim | priority: blocker | resolution: fixed

2012-09-27 11:14:08: fstapper@win.tue.nl created the issue

After linearizing the specification:

glob DC: Nat;
act a,b,c: Nat;
init comm({a|b->c}, a(0)| b(DC));

we get:

glob DC: Nat;

proc P(s3_P2: Pos) #        (s3_P2= 2) ->
         Terminate .
         P(s3_P2 = 3)
     + (s3_P2 ## 1 && !(DC 0)) ->
         a(DC)|b(0) .
         P(s3_P2 = 2)
     + (s3_P2 ## 1 && DC 0) ->
         c(DC) .
         P(s3_P2 = 2)
     + delta;

init P(1);

During simulation, the following transitions are enabled from the initial state:

initial state: [r1](../commit/27180ff2e)
0: a(DC)|b(0)  ->  [r2](../commit/480c7c610)
1: c(DC)  ->  [r2](../commit/480c7c610)

The only transition that should be enabled is:

0: c(0)  ->  [r1](../commit/27180ff2e)

version: mCRL2 toolset 201202.0.11119 (Release)

jgroote commented 12 years ago

2012-09-30 15:14:10: @jkeiren changed priority from major to blocker

jgroote commented 12 years ago

2012-09-30 15:14:10: @jkeiren changed status from new to accepted

jgroote commented 12 years ago

2012-09-30 15:14:10: @jkeiren changed owner from s051072 to jkeiren

jgroote commented 12 years ago

2012-09-30 15:14:10: @jkeiren

jgroote commented 12 years ago

2012-09-30 15:14:10: @jkeiren commented

Bug #1075 is a duplicate of this bug. An additional example was provided by jfg.

act a;
map b:Bool;
init b->a.delta;
jgroote commented 12 years ago

2012-09-30 15:18:46: @jkeiren changed status from accepted to closed

jgroote commented 12 years ago

2012-09-30 15:18:46: @jkeiren set resolution to fixed

jgroote commented 12 years ago

2012-09-30 15:18:46: @jkeiren commented

(In r11122) 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.

jgroote commented 12 years ago

2012-10-02 09:31:22: @jkeiren commented

(In 11135) Merge r11122, r11129 from trunk

r11122: 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. r11129: [release] Improve the error message introduced in r11122.

jgroote commented 12 years ago

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

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

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

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

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

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

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

(mCRL2-gui-qt) Finished implementation.

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.

(LTSGraph-qt) Implemented TikZ rendering.

Resolves #1027

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

Resolves #1025

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

Conflicts:

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

Fix build of compiling rewriter (broken in r10737)

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

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

Conflicts:

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

(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.

(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.

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

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.

(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.

Conflicts:

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

Conflicts:

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

Fixes #991.

Conflicts:

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

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

Conflicts:

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

Conflicts:

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

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

Conflicts:

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

Conflicts:

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

Fix build

Conflicts:

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

Conflicts:

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

Conflicts:

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

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.

(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.

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.

(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

Conflicts:

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

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

Fix by jkeiren

Add package script for Jenkins

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

Remove stray line from package script

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

Conflicts:

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

Fix build

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.

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

Fixed Bundle installation when using official QtSDK.

Removed superfluous linking to Boost libraries.

Conflicts: libraries/utilities/include/mcrl2/utilities/test_utilities.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

(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

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

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

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.

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

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

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.

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.

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.

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

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

Removed superfluous file, spotted by Wieger.

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

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

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.

[release] Fix a bunch of CLang compiler warnings

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

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

Conflicts: libraries/data/test/enumerator_test.cpp

Conflicts: libraries/process/test/process_test.cpp

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

[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

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

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

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

[release]

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

Layout improvement of mCRL2-gui.

[release]

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 "

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

[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.

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

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

Conflicts: libraries/lps/test/suminst_test.cpp

Conflicts: libraries/lps/test/symbolic_reachability_test.cpp

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

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 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

Conflicts: tools/lpsparunfold/lpsparunfoldlib.cpp

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

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

Added option that enables filepicker to open a file.

Fixes #1096

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

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.

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

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

Conflicts: libraries/core/build/mcrl2_classes.py

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

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

Removed obsolete "macosx" folder

Changed MCRL2_SINGLE_BUNDLE into MCRL2_OSX_PACKAGE.

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

Clean up some tests.

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.

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

Fixes #1112

Fix build

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