Remove mcrl2_gui_tool.h, and all uses

jgroote commented 12 years ago

Issue migrated from trac ticket # 1078

component: Utilities Library | priority: minor | resolution: fixed

2012-10-02 09:23:02: @jkeiren created the issue

The class mcrl2_gui_tool (in the utilities library) was used for creating wxWidgets interfaces. The QT implementation of mcrl2-gui does not need the functionality provided by this class, so it should be removed.

jgroote commented 12 years ago

2012-10-02 09:23:08: @jkeiren changed status from new to accepted

jgroote commented 12 years ago

2012-10-02 09:23:08: @jkeiren changed owner from wieger to jkeiren

jgroote commented 11 years ago

2012-11-12 09:52:52: @jkeiren changed status from accepted to closed

jgroote commented 11 years ago

2012-11-12 09:52:52: @jkeiren set resolution to fixed

jgroote commented 11 years ago

2012-11-12 09:52:52: @jkeiren commented

(In r11371) Remove traces of the mcrl2_gui_tool class. Fixes #1078.

This class has become superfluous with the move to the QT based tools.

jgroote commented 11 years ago

2012-11-13 08:23:25: @jkeiren commented

(In r11381) Merge revisions up to r11353 from trunk

Made a separate function to print conditions of conditional expressions, since an optimization in the print_condition for data expressions is not applicable.
Print an empty block set as {}, instead of omitting it.
Applied several fixes to both the specification and the implementation of push_allow. Most of these problems were found using random testing. The only failures left are test cases containing a tau, which apparently needs special handling.

Conflicts: libraries/process/include/mcrl2/process/utility.h

Decoupled alphabet and push_allow, since it has become clear that nothing can be reused.

Conflicts: libraries/process/include/mcrl2/process/alphabet.h

Moved operations on alphabets to a separate namespace, and renamed them. Now process expressions like comm, allow, merge, ... have corresponding alphabet operations with the same name. Inverse operations are defined when applicable (comm_inverse etc.).

Add test case for bug #1110.

It seems the bug is invalid. I have added a verbose message to indicate that the maximum number of states has been reached.

Added a space in the help message.

As agreed removed examples that use the n-parallel construct as it does not work anymore. Changed the 10 dining philosophers such that there are now 10 explicit parallel processes. Added the old construct to ticket #977, such that it is not forgotten.

Fixes #1114.

This problem was caused by a wrong implementation/definition of the inverse of a renaming operator (which was treated as if it were a bijection). The problem already shows up on the following simple example:

act c,d; init allow({c}, rename({d -> c}, c));

The problem has been fixed, awaiting the new implementation of alphabet conversions.

It might be that more random testing will reveal other bugs in the current implementation of the alphabet reductions.

Introduced the type allow_set.

Conflicts: libraries/process/include/mcrl2/process/alphabet.h

Added special handling for the value tau. Now the random tests succeed.
Print an empty multi_action_name as "tau".
Fixed handling of the rename operator. A block of the left hand sides of rename expressions had to be added.
Made a new implementation of rename_inverse.
Improved debugging. Now the algorithm displays in detail all the rewrite steps of alphabet reduction.
Removed the data rewriter parameter of compute_source, since it isn't used (noted by Jeroen).

Remove traces of the mcrl2_gui_tool class. Fixes #1078.

This class has become superfluous with the move to the QT based tools.

Conflicts: tools/besinfo/besinfo.cpp tools/bespp/bespp.cpp tools/bessolve/bessolve.cpp tools/complps2pbes/complps2pbes.cpp tools/lps2lts/lps2lts.cpp tools/lps2pbes/lps2pbes.cpp tools/lpsactionrename/lpsactionrename.cpp tools/lpsbinary/lpsbinary.cpp tools/lpsconfcheck/lpsconfcheck.cpp tools/lpsconstelm/lpsconstelm.cpp tools/lpsinfo/lpsinfo.cpp tools/lpsinvelm/lpsinvelm.cpp tools/lpsparelm/lpsparelm.cpp tools/lpsparunfold/lpsparunfold.cpp tools/lpspp/lpspp.cpp tools/lpsrewr/lpsrewr.cpp tools/lpssumelm/lpssumelm.cpp tools/lpssuminst/lpssuminst.cpp tools/lpsuntime/lpsuntime.cpp tools/lts2lps/lts2lps.cpp tools/lts2pbes/lts2pbes.cpp tools/ltscompare/ltscompare.cpp tools/ltsconvert/ltsconvert.cpp tools/ltsinfo/ltsinfo.cpp tools/mcrl22lps/mcrl22lps.cpp tools/mcrl2i/mcrl2i.cpp tools/mcrl2parse/mcrl2parse.cpp tools/pbes2bes/pbes2bes.cpp tools/pbes2bool/pbes2bool.cpp tools/pbesabsinthe/pbesabsinthe.cpp tools/pbesconstelm/pbesconstelm.cpp tools/pbesinfo/pbesinfo.cpp tools/pbesparelm/pbesparelm.cpp tools/pbespgsolve/pbespgsolve.cpp tools/pbespp/pbespp.cpp tools/pbesrewr/pbesrewr.cpp tools/pbesstategraph/pbesstategraph.cpp tools/symbolic_exploration/symbolic_exploration.cpp tools/tbf2lps/tbf2lps.cpp tools/tracepp/tracepp.cpp tools/txt2bes/txt2bes.cpp tools/txt2lps/txt2lps.cpp tools/txt2pbes/txt2pbes.cpp

Cleaned up the script for random testing of alphabet reduction.

Remove superfluous test targets.

Ammends r11371

Fix maintainer flags on MacOSX.

Allow associating multiple file types with one extension. Fixes #1111.

Note that a proper solution should be constructed, where the XML for a tool contains the supported input and output types.

Conflicts: tools/mcrl2-gui/toolcatalog.h

Fixed handling of nested allows. The case of an allow set that includes all subsets was not handled properly. Found using onebit.mcrl2.
Added alphabet operations operating on allow_set, implemented in terms of alphabet operations on multi_action_name_set. This is done to handle the case with include_subsets == true consistently.
Added some missing cases for alphabet operations for the case include_subsets == true.
Added tests.

Conflicts: libraries/process/include/mcrl2/process/alphabet.h libraries/process/test/alphabet_test.cpp

Fixed the subsets function. This makes alphabet reduction of onebit.mcrl2 succeed.

Fix build

mCRL2org / mCRL2