mcrl2ide TODO

[Valo13]

This issue describes features, enhancements and bugs that are planned to be addressed in the (near) future for mcrl2ide. Feel free to add anything yourself by leaving a comment.

FEATURES

• Allow parsing all properties with main parse button + show on properties dock whether a property is valid
• More code editor functionality (auto completion)
• Add example projects and a tutorial
• Import specification / create project from specification

ENHANCEMENTS

• Disallow concurrent runs of mcrl22lps
• Improve parsing feedback (parsing button, console, add/edit property dialog)
• Ask to save changes in case nothing was saved before
• Move "Add Property" button to properties dock
• Add more functionality concerning the specification only mode (new spec, open spec etc)
• Allow to edit the ordering of properties
• Make the abort buttons that correspond to toolbuttons that run tools more visible
• Improve ui in Mac dark mode (syntax highlighting)
• Improve equivalence checking usage
• When running a tool, save the specification in the in the temp folder; only save spec in project folder when "save" is chosen by user
• Add feedback to the property name field in the property dialog in case a character is entered that is not allowed

BUGS

• After aborting a process that generates a file, running it again uses the generated file due to caching, even though it is incomplete
• Cannot choose existing folder when creating/saving project
• On some screens (Tim's Mac) the icons of the property dock buttons go outside of the button boundary
• "Open project in explorer" does not work on mac

Last updated 20-6-2022

Finished tasks

FEATURES

• Shortcuts for tools
• Import property from file
• Clear console
• Show project folder in file explorer
• Check for external project changes on focus
• Resize property dock on opening project or adding/editing property to fit the property names
• Specification editing only mode + allow specification file as command line argument
• Allow users to save intermediate files
• Equivalence checking

ENHANCEMENTS

• Check existence of used tool executables on startup
• Set the ordering of the properties on the properties dock
• When the property name is too long for the properties dock, show it from start instead of from end
• Add more equivalences for reduction, distinguish abstraction
• Allow to abort property parsing in add/edit property dialog while staying in this dialog
• Add syntax highlighting for matching parentheses

BUGS

• On linux the width of the properties dock resets to default when changing from/to fullscreen, when hovering the mouse on the edge of the properties dock slowly and when running tools
• In case of a parsing error the cursor does not jump to the location of the problem properly in case it is below lines that are wrapped around

[FWDekker]

When working using git I will often check out a different branch. When I do this the IDE gives me a prompt asking me if I want to reload the code. I think it would be useful if this feature would also detect changes in the project's properties and would reload them if the user so desires.

[Valo13]

@FWDekker Good point, I'll work on this tomorrow

[Valo13]

@FWDekker By commit d2e102d948c7bb20fb516e8d4a70751f0a7768bb mcrl2ide will ask for a reload also when the project file or a property file has changed from outside. To get this version of the tool, try the nightly build tomorrow. Note that the format for some files such as .lts files has changed since the last release, but this doesn't affect the usage of mcrl2ide.

[FWDekker]

Awesome! I'll try it out tomorrow.

[jkeiren]

@Valo13 You may want to add the following enhancement: When the find and replace window is open, and the focus is on the main window, issuing the command `find and replace' should move the focus to the find and replace window.

This is standard behaviour in most editors, and not refocusing the window is confusing.

[Jhpmeer]

I would like to propose a feature or enhancement of the IDE that deals with the task of commenting out multiple lines. Right now this can be a repetitive and time consuming task.

There are editors with the ability to comment highlighted code. Here, you select a section of code encompassing multiple lines and press some shortcut e.g. 'cmd + /' or 'ctrl + /'. The selected lines will then be commented. Likewise for un-commenting. An example from the atom editor. I have looked through the menus and asked around, but there seems to be no such feature.

I believe this can be a very useful feature and a 'quality of life' improvement. Others to which I have pitched the idea agree. Hence, my comment here.

[Jhpmeer]

I found a bug in the IDE in the opening of projects.

Let us assume the case where we have two distinct projects A and B. The contents of the specification is different and the properties are different. However, the name of the specification file is the same.

After starting the IDE, I can open project A and view the state space or verify properties, the IDE behaves as expected. Now, when I consecutively open project B, then the IDE visually loads the correct specification and properties of project B. However, when I try to view the state space it will show the state space of project A. And when I try to prove any property of project B, it will try to prove this property for the specification of project A.

I have verified by means of some testing that this relies on the name of the specification file. If the name of the specification files is not equal, the IDE behaves as expected.

Note that viewing of the state space or verifying a propery inbetween the opening of project A and B is mandatory for the occurrance of this bug. If one opens project A and immediately thereafter open project B, this bug will not occur.

[Valo13]

Thanks for the detailed bug report. Are the project names the same as well? The project name is determined by the base name of the file with the extension .mcrl2proj. If so, this sounds like this has to do with caching. Since the project names are the same, all generated file names are the same as well. I would expect that when you generate the state space for project B the console prints messages like "LPS already exists" and that after you modify the spec of project B it generates the state space correctly.

Were you able to generate a test case for this using the IDE only or did you need to adapt file names manually?

[Jhpmeer]

Indeed, the project names are the same. Whenever I generate the state space of project B the console displays the following message:

Up to date LPS lready exists .#### SHOWING LTS ####

Interestingly enough it does so twice. Furtmermore, after modifying the spec of project B the IDE shows the correct state space. To this end, it is as you expected.

I attempted generating the test case using the IDE only. But this does not seem possible. I found only two ways to recreate this bug:

1. Adapting the file names of the .mcrl2 and .mcrl2proj files of project B and the contents of the .mcrl2proj file to match this change
2. Make a copy of the project folder of project A and adapt the specification and properties through the IDE

I can see how this issue does not come up in normal use. However, I encountered this issue in a demonstration of the toolset where I compared my current model with an older iteration. Hence why the project and file names where equal. Luckily nobody noticed that the IDE was giving errors with the verifying of properties in the demonstration. But it could have been quite painful.

[Valo13]

Thanks for the reply, I will work on a fix some time this week.

[Jhpmeer]

I found a bug in how the project names are handled in the IDE.

Let us assume the case where we will create a new project. The new project name has a dot in it. For example:

Some project v0.2

Then the IDE will create the appropriate folders and files. Everything behaves as expected.

However, when we close the IDE and reopen the project we can observe at the top of the window the IDE shows:

mCRL2 IDE - some project v0

The project name is stripped from the file name up until the first dot. Now, when we add a new property and save it we can observe how in the project folder a new file has been created:

some project v0.mcrl2proj

When we now close the IDE and reopen the project again we are greeted by a message saying:

Provided folder contains more than one project file

This is obviously the case from the above observation that a new project file has been created. Now, we can delete the faulty project file with the wrong name from the project folder. However, we lose the link to our earlier created property. Moreover, this issue will keep reappering every time we add a property and reopen a project. We can also delete the (original) project file with the correct name, The IDE will behave as expected henceforth. But this is not the prettiest solution.

[Valo13]

Hmm, this is indeed unwanted behaviour, I'll look into it. It seems to be due to a mistake in reading the project name from the project file. Thanks for the bug report.

[Jhpmeer]

I found a bug in the Zoom In/Out feature of the IDE.

Let us assume we have a project where the specification is of a length that does not normally fit in the window and we have to scroll.

If I scroll to the bottom of the file and I zoom in (either by CTR + =, or CTRL + scroll), sometimes the bottom few lines will fall below the window and I cannot scroll down to see them. For example, my project has 81 lines, I zoom in and the issue occurs. Now I can see up to the 77-th line and I can see a sliver of the 78-th line. I cannot scroll down to see the lines 78-81.

Depending on the size of the file I have scroll up either a bit or to the top and the scrollbar on the right visually shortens (to the correct size). And now I can scrol to the last lines again.

The inverse can also happen where, when zooming out, extra space is added at the end (below) of the file. Again, scrolling up (to the top) fixes this issue.

At first I thought this was related to the line wrap-around issue. But I have verified that this is not the case.

I hope this explanation is somewhat clear. I think the issue is minor. But I wanted to share it nontheless.

[Valo13]

Hmm, I can't seem to reproduce the bug you describe when zooming in. When I move to the bottom of the file and zoom in two things happen depending on zoom level:

• A number of lines are pushed below the window. The vertical slider automatically updates (shortens and moves up) such that I can directly scroll down to the last line.
• The last line is still/again in the window

I can reproduce the bug you describe when zooming out but I feel like that is not really a problem.

What OS do you use?

[Jhpmeer]

I use windows 10. Specifically on a laptop the TU/e issued for students in 2017.