probcli's ability to read RODIN ".eventb" exports
6 views
Skip to first unread message
Paul Simon
Jul 18, 2025, 4:30:46 AMJul 18
to ProB Users
Michael Leuschel
Jul 18, 2025, 6:31:56 AMJul 18
to Paul Simon, ProB Users
Hi Paul,
what do you mean by absorb “.eventb” exports.
They should work, provided you use a reasonably recent ProB version.
You can either use the nightly version or the latest stable version 1.15.0.
If this does not work please send us details about the exact problem.
Kind regards,
Michael
> On 18 Jul 2025, at 10:30, Paul Simon <ment...@gmail.com> wrote:
>
> I was wondering when probcli will be able to absorb ".eventb" exports from RODIN (3.9). Is there a known answer?
>
> --
> You received this message because you are subscribed to the Google Groups "ProB Users" group.
> To unsubscribe from this group and stop receiving emails from it, send an email to prob-users+...@googlegroups.com.
> To view this discussion visit https://groups.google.com/d/msgid/prob-users/d9ce1518-1c75-4220-9f62-cd277d1acb37n%40googlegroups.com.
what do you mean by absorb “.eventb” exports.
They should work, provided you use a reasonably recent ProB version.
You can either use the nightly version or the latest stable version 1.15.0.
If this does not work please send us details about the exact problem.
Kind regards,
Michael
> On 18 Jul 2025, at 10:30, Paul Simon <ment...@gmail.com> wrote:
>
> I was wondering when probcli will be able to absorb ".eventb" exports from RODIN (3.9). Is there a known answer?
>
> You received this message because you are subscribed to the Google Groups "ProB Users" group.
> To unsubscribe from this group and stop receiving emails from it, send an email to prob-users+...@googlegroups.com.
> To view this discussion visit https://groups.google.com/d/msgid/prob-users/d9ce1518-1c75-4220-9f62-cd277d1acb37n%40googlegroups.com.
Michael Leuschel
Jul 18, 2025, 9:47:45 AMJul 18
to Paul Simon, ProB Users
Hi Paul,
probcli does not really have an interactive animator, although it would be quite easy to add.
Using the REPL (Read-Eval-Print-Loop) you can sort of use it as an interactive animator (we could add one or two more commands e.g. to show the enabled transitions in the current state).
In the transcript below you can see a few commands, type :help in the REPL to see more:
probcli FILE.eventb -init -repl
ProB Interactive Expression and Predicate Evaluator
Type ":help" for more information.
>>> :state
Current state id 1 : ( ctr=0 &
inc=1 )
>>> -animate 1
Executing probcli command: [cli_random_animate(1,true)]
>>> :states
Statespace: 4 states (3 processed) and 4 transitions.
>>> :statespace
State ID root (root/0)
-> 0 ($setup_constants/0)
State ID 0 (concrete_constants/1)
-> 1 ($initialise_machine/0)
State ID 1 (const_and_vars/2)
-> 2 (Increment/0)
-> 1 (-->/2)
State ID 2 (const_and_vars/2)
Current State ID 1
Note: you can also use ProB2-UI to interactively animate the .eventb file.
Greetings,
Michael
> On 18 Jul 2025, at 14:57, Paul Simon <ment...@gmail.com> wrote:
>
> Hi Michael
>
> I have just realised i did a mistake in my interpretation !
>
>
> 1/ Just 2 days before I download prob v1.15
>
> 2/ I export a very small machine from RODIN 1.9 thanks to the function « export for use in ProB standalone"
>
probcli does not really have an interactive animator, although it would be quite easy to add.
Using the REPL (Read-Eval-Print-Loop) you can sort of use it as an interactive animator (we could add one or two more commands e.g. to show the enabled transitions in the current state).
In the transcript below you can see a few commands, type :help in the REPL to see more:
probcli FILE.eventb -init -repl
ProB Interactive Expression and Predicate Evaluator
Type ":help" for more information.
>>> :state
Current state id 1 : ( ctr=0 &
inc=1 )
>>> -animate 1
Executing probcli command: [cli_random_animate(1,true)]
>>> :states
Statespace: 4 states (3 processed) and 4 transitions.
>>> :statespace
State ID root (root/0)
-> 0 ($setup_constants/0)
State ID 0 (concrete_constants/1)
-> 1 ($initialise_machine/0)
State ID 1 (const_and_vars/2)
-> 2 (Increment/0)
-> 1 (-->/2)
State ID 2 (const_and_vars/2)
Current State ID 1
Note: you can also use ProB2-UI to interactively animate the .eventb file.
Greetings,
Michael
> On 18 Jul 2025, at 14:57, Paul Simon <ment...@gmail.com> wrote:
>
> Hi Michael
>
> I have just realised i did a mistake in my interpretation !
>
>
> 1/ Just 2 days before I download prob v1.15
>
> 2/ I export a very small machine from RODIN 1.9 thanks to the function « export for use in ProB standalone"
>
Michael Leuschel
Jul 20, 2025, 3:33:17 AMJul 20
to Paul Simon, ProB Users
Dear Paul,
there are several alternatives:
- you can use VisB in ProB2-UI to create SVG/HTML based interactive visualisations.
Link: https://prob.hhu.de/w/index.php?title=VisB
This has been used by our group and by others to create interactive prototypes,
see, e.g., https://link.springer.com/chapter/10.1007/978-3-031-33163-3_22, https://link.springer.com/chapter/10.1007/978-3-031-33163-3_24
for an air-traffic control system.
- you can use the ProB2-Java-API (https://github.com/hhu-stups/prob2_kernel) to embed ProB into a Java application.
This has been used by several users to build their own tool or prototype on top of ProB.
One example is Meeduse (see e.g., https://hal.science/hal-03012213/file/iFM_2020_idani.pdf)
or this prototype https://link.springer.com/article/10.1007/s10009-020-00551-6 for a real-life usage to control trains using Hybrid-Level 3 principles.
Greetings,
Michael
> On 18 Jul 2025, at 17:22, Paul Simon <ment...@gmail.com> wrote:
>
> thank you Michael for your explanations which were very useful
>
>
> 1/ I tried "probcli FILE.eventb -init -repl »
>
> This corresponds quite well to what I'm looking for, but it lacks the deterministic aspect, unless we can choose the event and the associated parameters?
>
> 2/ I downloaded Prob2-UI and it works well
>
> 3/ but perhaps I should start by explaining the goal pursued
>
> I am looking to model information systems, first in a "black box"
> but to validate the models created I have to rely on the opinion of the end users.
> For this I try to put in their hands something that resembles the final target
> what an end user of the information system perceives are menus and forms (as is ProB and ProB2-UI).
> To quickly present menus and forms to users, what better than a software engineering tool (IBM Eclipse or Microsoft Visual Studio, etc.)
>
> Ultimately, the result to be produced with good productivity would be a set consisting of:
> - a first part, which would be an executable produced by a software engineering tool
> - a second part, which would be the B model that carries the expected target functionality
> The first part is simply a skin that continuously requests the second part
>
> How do you imagine the mechanics to be put in place with the ProB tools currently available?
>
> best regards
>
> Paul
>> <GraphiqueCollé-1.tiff>
>>>
>>>
>>> 3/ I launched proB and open file exported.
>>>
>>> It worked well
>>>
>> <GraphiqueCollé-2.tiff>
>>>
>>>
>>>
>>> 4/ then i tried the following test :
>>>
>> <GraphiqueCollé-3.tiff>
>>>
>>>
>>> it works well too
>>>
>>> 5/ i tried to animate the machine step by step as i can do with the IDE « proB"
>>>
>>> I did not find the right command to use until now I think
>>>
>>> How can I do ?
>>>
>>> I tried
>>> probcli -animate 1 m00_mch.eventb
>>> probcli -execute 1 m00_mch.eventb
>>>
>>> the process stops at each trial
>>>
>>> best regards
>>>
>>> Paul
>>>>
>>>>
there are several alternatives:
- you can use VisB in ProB2-UI to create SVG/HTML based interactive visualisations.
Link: https://prob.hhu.de/w/index.php?title=VisB
This has been used by our group and by others to create interactive prototypes,
see, e.g., https://link.springer.com/chapter/10.1007/978-3-031-33163-3_22, https://link.springer.com/chapter/10.1007/978-3-031-33163-3_24
for an air-traffic control system.
- you can use the ProB2-Java-API (https://github.com/hhu-stups/prob2_kernel) to embed ProB into a Java application.
This has been used by several users to build their own tool or prototype on top of ProB.
One example is Meeduse (see e.g., https://hal.science/hal-03012213/file/iFM_2020_idani.pdf)
or this prototype https://link.springer.com/article/10.1007/s10009-020-00551-6 for a real-life usage to control trains using Hybrid-Level 3 principles.
Greetings,
Michael
> On 18 Jul 2025, at 17:22, Paul Simon <ment...@gmail.com> wrote:
>
> thank you Michael for your explanations which were very useful
>
>
> 1/ I tried "probcli FILE.eventb -init -repl »
>
> This corresponds quite well to what I'm looking for, but it lacks the deterministic aspect, unless we can choose the event and the associated parameters?
>
> 2/ I downloaded Prob2-UI and it works well
>
> 3/ but perhaps I should start by explaining the goal pursued
>
> I am looking to model information systems, first in a "black box"
> but to validate the models created I have to rely on the opinion of the end users.
> For this I try to put in their hands something that resembles the final target
> what an end user of the information system perceives are menus and forms (as is ProB and ProB2-UI).
> To quickly present menus and forms to users, what better than a software engineering tool (IBM Eclipse or Microsoft Visual Studio, etc.)
>
> Ultimately, the result to be produced with good productivity would be a set consisting of:
> - a first part, which would be an executable produced by a software engineering tool
> - a second part, which would be the B model that carries the expected target functionality
> The first part is simply a skin that continuously requests the second part
>
> How do you imagine the mechanics to be put in place with the ProB tools currently available?
>
> best regards
>
> Paul
>>>
>>>
>>> 3/ I launched proB and open file exported.
>>>
>>> It worked well
>>>
>> <GraphiqueCollé-2.tiff>
>>>
>>>
>>>
>>> 4/ then i tried the following test :
>>>
>> <GraphiqueCollé-3.tiff>
>>>
>>>
>>> it works well too
>>>
>>> 5/ i tried to animate the machine step by step as i can do with the IDE « proB"
>>>
>>> I did not find the right command to use until now I think
>>>
>>> How can I do ?
>>>
>>> I tried
>>> probcli -animate 1 m00_mch.eventb
>>> probcli -execute 1 m00_mch.eventb
>>>
>>> the process stops at each trial
>>>
>>> best regards
>>>
>>> Paul
>>>
>>>
>>>
>>>
>>>
>>>
>>>> Le 18 juil. 2025 à 12:31, Michael Leuschel <michael....@gmail.com> a écrit :
>>>>
>>>> Hi Paul,
>>>>
>>>> what do you mean by absorb “.eventb” exports.
>>>> They should work, provided you use a reasonably recent ProB version.
>>>> You can either use the nightly version or the latest stable version 1.15.0.
>>>> If this does not work please send us details about the exact problem.
>>>>
>>>> Kind regards,
>>>> Michael
>>>
>>>
>>>
>>>
>>>
>>>> Le 18 juil. 2025 à 12:31, Michael Leuschel <michael....@gmail.com> a écrit :
>>>>
>>>> Hi Paul,
>>>>
>>>> what do you mean by absorb “.eventb” exports.
>>>> They should work, provided you use a reasonably recent ProB version.
>>>> You can either use the nightly version or the latest stable version 1.15.0.
>>>> If this does not work please send us details about the exact problem.
>>>>
>>>> Kind regards,
>>>>
>>>>
Paul Simon
Jul 22, 2025, 1:16:05 AMJul 22
to Michael Leuschel, ProB Users
thank you Michael for your explanations which were very useful
1/ I tried "probcli FILE.eventb -init -repl »
This corresponds quite well to what I'm looking for, but it lacks the deterministic aspect, unless we can choose the event and the associated parameters?
2/ I downloaded Prob2-UI and it works well
3/ but perhaps I should start by explaining the goal pursued
I am looking to model information systems, first in a "black box"
but to validate the models created I have to rely on the opinion of the end users.
For this I try to put in their hands something that resembles the final target
what an end user of the information system perceives are menus and forms (as is ProB and ProB2-UI).
To quickly present menus and forms to users, what better than a software engineering tool (IBM Eclipse or Microsoft Visual Studio, etc.)
Ultimately, the result to be produced with good productivity would be a set consisting of:
- a first part, which would be an executable produced by a software engineering tool
- a second part, which would be the B model that carries the expected target functionality
The first part is simply a skin that continuously requests the second part
How do you imagine the mechanics to be put in place with the ProB tools currently available?
best regards
Paul
> Le 18 juil. 2025 à 15:47, Michael Leuschel <michael....@gmail.com> a écrit :
>
1/ I tried "probcli FILE.eventb -init -repl »
This corresponds quite well to what I'm looking for, but it lacks the deterministic aspect, unless we can choose the event and the associated parameters?
2/ I downloaded Prob2-UI and it works well
3/ but perhaps I should start by explaining the goal pursued
I am looking to model information systems, first in a "black box"
but to validate the models created I have to rely on the opinion of the end users.
For this I try to put in their hands something that resembles the final target
what an end user of the information system perceives are menus and forms (as is ProB and ProB2-UI).
To quickly present menus and forms to users, what better than a software engineering tool (IBM Eclipse or Microsoft Visual Studio, etc.)
Ultimately, the result to be produced with good productivity would be a set consisting of:
- a first part, which would be an executable produced by a software engineering tool
- a second part, which would be the B model that carries the expected target functionality
The first part is simply a skin that continuously requests the second part
How do you imagine the mechanics to be put in place with the ProB tools currently available?
best regards
Paul
> Le 18 juil. 2025 à 15:47, Michael Leuschel <michael....@gmail.com> a écrit :
>
> <GraphiqueCollé-1.tiff>
>>
>>
>> 3/ I launched proB and open file exported.
>>
>> It worked well
>>
> <GraphiqueCollé-2.tiff>
>>
>>
>>
>> 4/ then i tried the following test :
>>
> <GraphiqueCollé-3.tiff>
>>
>>
>> it works well too
>>
>> 5/ i tried to animate the machine step by step as i can do with the IDE « proB"
>>
>> I did not find the right command to use until now I think
>>
>> How can I do ?
>>
>> I tried
>> probcli -animate 1 m00_mch.eventb
>> probcli -execute 1 m00_mch.eventb
>>
>> the process stops at each trial
>>
>> best regards
>>
>> Paul
>>
>>
>>
>>
>>
>>
>>> Le 18 juil. 2025 à 12:31, Michael Leuschel <michael....@gmail.com> a écrit :
>>>
>>
>>
>> 3/ I launched proB and open file exported.
>>
>> It worked well
>>
> <GraphiqueCollé-2.tiff>
>>
>>
>>
>> 4/ then i tried the following test :
>>
> <GraphiqueCollé-3.tiff>
>>
>>
>> it works well too
>>
>> 5/ i tried to animate the machine step by step as i can do with the IDE « proB"
>>
>> I did not find the right command to use until now I think
>>
>> How can I do ?
>>
>> I tried
>> probcli -animate 1 m00_mch.eventb
>> probcli -execute 1 m00_mch.eventb
>>
>> the process stops at each trial
>>
>> best regards
>>
>> Paul
>>
>>
>>
>>
>>
>>
>>> Le 18 juil. 2025 à 12:31, Michael Leuschel <michael....@gmail.com> a écrit :
>>>
>>> Hi Paul,
>>>
>>> what do you mean by absorb “.eventb” exports.
>>> They should work, provided you use a reasonably recent ProB version.
>>> You can either use the nightly version or the latest stable version 1.15.0.
>>> If this does not work please send us details about the exact problem.
>>>
>>> Kind regards,
>>> Michael
>>>
>>> what do you mean by absorb “.eventb” exports.
>>> They should work, provided you use a reasonably recent ProB version.
>>> You can either use the nightly version or the latest stable version 1.15.0.
>>> If this does not work please send us details about the exact problem.
>>>
>>> Kind regards,
>>>
>>>
Paul Simon
Jul 22, 2025, 1:16:05 AMJul 22
to Michael Leuschel, ProB Users
Hi Michael
I have just realised i did a mistake in my interpretation !
1/ Just 2 days before I download prob v1.15
2/ I export a very small machine from RODIN 1.9 thanks to the function « export for use in ProB standalone"
3/ I launched proB and open file exported.
It worked well
4/ then i tried the following test :
it works well too
5/ i tried to animate the machine step by step as i can do with the IDE « proB"
I did not find the right command to use until now I think
How can I do ?
I tried
probcli -animate 1 m00_mch.eventb
probcli -execute 1 m00_mch.eventb
the process stops at each trial
best regards
Paul
Le 18 juil. 2025 à 12:31, Michael Leuschel <michael....@gmail.com> a écrit :
Paul Simon
Jul 22, 2025, 12:12:22 PMJul 22
to Michael Leuschel, ProB Users
Thank you Michael for all the informations
i have just begun to analyse.
I understand that ProB2-Java-API best meets my needs.
I've looked at all the tools I need to master. None of them are familiar to me at the moment.
So it's going to take me a while to produce a first functional result!
Greetings
Paul
i have just begun to analyse.
I understand that ProB2-Java-API best meets my needs.
I've looked at all the tools I need to master. None of them are familiar to me at the moment.
So it's going to take me a while to produce a first functional result!
Greetings
Paul
Michael Leuschel
Jul 23, 2025, 7:18:55 AMJul 23
to Paul Simon, ProB Users
Hi Paul,
what exactly is the problem?
I was able to open and animate the model in ProB Tcl/Tk and ProB2-UI.
> On 23 Jul 2025, at 12:01, Paul Simon <ment...@gmail.com> wrote:
>
> for the third the loading seems to be difficult
> is there something i have to do ?
Greetings,
Michael
what exactly is the problem?
I was able to open and animate the model in ProB Tcl/Tk and ProB2-UI.
> On 23 Jul 2025, at 12:01, Paul Simon <ment...@gmail.com> wrote:
>
> for the third the loading seems to be difficult
> is there something i have to do ?
Greetings,
Michael
Paul Simon
Jul 23, 2025, 8:25:13 AMJul 23
to Michael Leuschel, ProB Users
when I am loading the file m10_mch.eventb the too ProB2-UI appears like this :
it then i tried to open another file the following text box appears :
if I choose to see the details and to copy paste i get this :
java.util.concurrent.CancellationException
at java.base/java.util.concurrent.CompletableFuture.cancel(Unknown Source)
at de.prob2.ui.internal.executor.CompletableFutureTask.access$001(CompletableFutureTask.java:18)
at de.prob2.ui.internal.executor.CompletableFutureTask$1.done(CompletableFutureTask.java:26)
at java.base/java.util.concurrent.FutureTask.finishCompletion(Unknown Source)
at java.base/java.util.concurrent.FutureTask.cancel(Unknown Source)
at de.prob2.ui.internal.executor.CompletableFutureTask.cancel(CompletableFutureTask.java:46)
at de.prob2.ui.internal.executor.CliTaskExecutor.lambda$interruptAll$2(CliTaskExecutor.java:86)
at java.base/java.lang.Iterable.forEach(Unknown Source)
at de.prob2.ui.internal.executor.CliTaskExecutor.interruptAll(CliTaskExecutor.java:86)
at de.prob2.ui.prob2fx.CurrentProject.startAnimation(CurrentProject.java:159)
at de.prob2.ui.prob2fx.CurrentProject.startAnimation(CurrentProject.java:170)
at de.prob2.ui.project.ProjectManager.openAutomaticProjectFromMachine(ProjectManager.java:313)
at de.prob2.ui.project.ProjectManager.openFile(ProjectManager.java:321)
at de.prob2.ui.menu.FileMenu.handleOpen(FileMenu.java:161)
at java.base/jdk.internal.reflect.NativeMethodAccessorImpl.invoke0(Native Method)
at java.base/jdk.internal.reflect.NativeMethodAccessorImpl.invoke(Unknown Source)
at java.base/jdk.internal.reflect.DelegatingMethodAccessorImpl.invoke(Unknown Source)
at java.base/java.lang.reflect.Method.invoke(Unknown Source)
at com.sun.javafx.reflect.Trampoline.invoke(MethodUtil.java:77)
at jdk.internal.reflect.GeneratedMethodAccessor27.invoke(Unknown Source)
at java.base/jdk.internal.reflect.DelegatingMethodAccessorImpl.invoke(Unknown Source)
at java.base/java.lang.reflect.Method.invoke(Unknown Source)
at com.sun.javafx.reflect.MethodUtil.invoke(MethodUtil.java:275)
at com.sun.javafx.fxml.MethodHelper.invoke(MethodHelper.java:84)
at javafx.fxml.FXMLLoader$MethodHandler.invoke(FXMLLoader.java:1854)
at javafx.fxml.FXMLLoader$ControllerMethodEventHandler.handle(FXMLLoader.java:1724)
at com.sun.javafx.event.CompositeEventHandler.dispatchBubblingEvent(CompositeEventHandler.java:86)
at com.sun.javafx.event.EventHandlerManager.dispatchBubblingEvent(EventHandlerManager.java:234)
at com.sun.javafx.event.EventHandlerManager.dispatchBubblingEvent(EventHandlerManager.java:191)
at com.sun.javafx.event.BasicEventDispatcher.dispatchEvent(BasicEventDispatcher.java:58)
at com.sun.javafx.event.EventDispatchChainImpl.dispatchEvent(EventDispatchChainImpl.java:114)
at com.sun.javafx.event.EventUtil.fireEventImpl(EventUtil.java:74)
at com.sun.javafx.event.EventUtil.fireEvent(EventUtil.java:49)
at javafx.event.Event.fireEvent(Event.java:198)
at javafx.scene.control.MenuItem.fire(MenuItem.java:459)
at com.sun.javafx.scene.control.GlobalMenuAdapter.lambda$bindMenuItemProperties$2(GlobalMenuAdapter.java:153)
at com.sun.javafx.event.CompositeEventHandler.dispatchBubblingEvent(CompositeEventHandler.java:86)
at com.sun.javafx.event.EventHandlerManager.dispatchBubblingEvent(EventHandlerManager.java:234)
at com.sun.javafx.event.EventHandlerManager.dispatchBubblingEvent(EventHandlerManager.java:191)
at com.sun.javafx.event.BasicEventDispatcher.dispatchEvent(BasicEventDispatcher.java:58)
at com.sun.javafx.event.EventDispatchChainImpl.dispatchEvent(EventDispatchChainImpl.java:114)
at com.sun.javafx.event.EventUtil.fireEventImpl(EventUtil.java:74)
at com.sun.javafx.event.EventUtil.fireEvent(EventUtil.java:54)
at javafx.event.Event.fireEvent(Event.java:198)
at javafx.scene.control.MenuItem.fire(MenuItem.java:459)
at com.sun.javafx.tk.quantum.GlassSystemMenu$1.action(GlassSystemMenu.java:234)
in Rodin i can animate the model with ProB plugin
greetings
Paul
Michael Leuschel
Jul 23, 2025, 9:38:14 AMJul 23
to Paul Simon, ProB Users
Hi,
have you used the Snapshot version of ProB2-UI?
If not, can you check if your problem persists with it?
The new ProB for Rodin plugin now also exports event descriptions, which older ProB versions cannot handle yet.
We have not yet released a new stable version for ProB2-UI yet with that feature.
Greetings,
Michael
have you used the Snapshot version of ProB2-UI?
If not, can you check if your problem persists with it?
The new ProB for Rodin plugin now also exports event descriptions, which older ProB versions cannot handle yet.
We have not yet released a new stable version for ProB2-UI yet with that feature.
Greetings,
Michael
Paul Simon
Jul 23, 2025, 9:44:28 AMJul 23
to Michael Leuschel, ProB Users
Michael
when I open « à propos de » i can see
ProB 2 UI :
Version : 1.2.1
Commit : c77c9db2ce44f1c467bdc4a35b6804c994ff9227
API Java ProB :
Version : 4.12.2
Commit : e28d23c5e078692f331e20f7453f9675cfb5bc90
ProB CLI :
Version : 1.12.2-final
Commit : 33deeb12d48dc4f8b6e7b3664d848500b9a06685
Modification dernière : Thu Aug 10 15:02:52 2023 +0200
Prolog : SICStus 4.7.1 (x86_64-darwin-18.7.0): Fri Jan 21 19:45:28 CET 2022
Parseur B de ProB :
Version : 2.12.7
Commit : aca8ecbba363bb08d15e49001ea18bea2e65541a
Java :
Version : 17.0.5 (Homebrew)
VM : OpenJDK 64-Bit Server VM
Version de VM : 17.0.5+0 (Homebrew)
JavaFX :
Version : 17.0.8
Version runtime : 17.0.8+2
Is it clearer ?
greetings
Michael Leuschel
Jul 23, 2025, 9:47:31 AMJul 23
to Paul Simon, ProB Users
Hi,
you have the stable version, which unfortunately is a bit old. We hope to release a new stable version based on probcli 1.15.0 soon.
In the meantime, please try a Snapshot version; links to download are provided here:
https://prob.hhu.de/w/index.php?title=Download#ProB2-UI_(based_on_JavaFX)
Greetings,
Michael
> On 23 Jul 2025, at 15:44, Paul Simon <ment...@gmail.com> wrote:
>
> Michael
>>>
>>
>
you have the stable version, which unfortunately is a bit old. We hope to release a new stable version based on probcli 1.15.0 soon.
In the meantime, please try a Snapshot version; links to download are provided here:
https://prob.hhu.de/w/index.php?title=Download#ProB2-UI_(based_on_JavaFX)
Greetings,
Michael
> On 23 Jul 2025, at 15:44, Paul Simon <ment...@gmail.com> wrote:
>
> Michael
>>>
>>
>
Paul Simon
Jul 23, 2025, 10:21:22 AMJul 23
to Michael Leuschel, ProB Users
Thanks for your answer Michael
I have installed but after having launched it stops right away !
i am actually using java version 21 (temurin) and macOS 10.15.17
i have not seen any prerequisite on macOS.
greetings
Paul
I have installed but after having launched it stops right away !
i am actually using java version 21 (temurin) and macOS 10.15.17
i have not seen any prerequisite on macOS.
greetings
Paul
Michael Leuschel
Jul 23, 2025, 11:58:07 AMJul 23
to Paul Simon, ProB Users
Hi Paul,
can you send us more details.
Can you try using the multiplatform jar and start it?
Greetings,
Michael
can you send us more details.
Can you try using the multiplatform jar and start it?
Greetings,
Michael
Paul Simon
Jul 24, 2025, 4:10:52 AMJul 24
to Michael Leuschel, ProB Users
I tried too on my PC (on which i am not the administrator)
I used then "prob2-ui-1.2.2-SNAPSHOT-multi.jar » (snapshot version)
It works well with m10_mch.eventb (that did not work with V1.2.1 on my mac)
greetings
Début du message réexpédié :
Michael Leuschel
Jul 25, 2025, 2:49:32 AMJul 25
to Paul Simon, ProB Users
Hi Paul,
yes, this is due to the minimum requirements of JavaFX:
ERROR: macOS version is 10.15, which is below the minimum of 11.0
So you would need to upgrade to maOS Big Sur (Nov 2020) or newer to use the latest ProB2-UI version.
Greetings,
Michael
yes, this is due to the minimum requirements of JavaFX:
ERROR: macOS version is 10.15, which is below the minimum of 11.0
So you would need to upgrade to maOS Big Sur (Nov 2020) or newer to use the latest ProB2-UI version.
Greetings,
Michael
Reply all
Reply to author
Forward
0 new messages