Checking Statecharts with JPF

[Tom-Soucies]

I'm working on a project where first I develop a statechart using the Itemis tool (https://www.itemis.com/en/products/itemis-create/documentation/user-guide/overview_what_are_itemis_create_statechart_tools?hsLang=en) which allows me to obtain Java classes from it.

I now want to prove some properties using JPF. So I followed the wiki to put it all together. I have a Java class Model that imports the Statechart class and models it. My aim is to make JPF checks properties on this model. The issue is that whatever parameters I try to change in JPF, I get an out of memory error. I tried with "-Xmx16g" (and I can't really do better) and it still does not work. Keep in mind that here I am working with a 4 states, 2 events, 2 variables statechart. My goal being to study way more complex statechart I'm woried.

Is there something I can do to optimize the memory I spend on my model or something I should do differently?
Here is the output for reference:

====================================================== system under test
Model.main()

====================================================== search started: 7/8/25, 4:50 PM
[WARNING] orphan NativePeer method: jdk.internal.misc.Unsafe.getUnsafe()Lsun/misc/Unsafe;
Starting modelling
Setting up the statemachine
Entering the statemachines

[SEVERE] JPF out of memory

====================================================== search constraint
JPF out of memory

====================================================== snapshot 
thread java.lang.Thread:{id:0,name:main,status:RUNNING,priority:5,isDaemon:false,lockCount:0,suspendCount:0}
  call stack:
	at Model.main(Model.java:78)

thread Model$Substracter:{id:1,name:Thread-1,status:RUNNING,priority:5,isDaemon:false,lockCount:0,suspendCount:0}
  call stack:

thread Model$Divider:{id:2,name:Thread-2,status:RUNNING,priority:5,isDaemon:false,lockCount:0,suspendCount:0}
  call stack:


====================================================== results
error #1: gov.nasa.jpf.vm.NoOutOfMemoryErrorProperty

====================================================== statistics
elapsed time:       00:26:41
states:             new=3,visited=0,backtracked=3,end=0
search:             maxDepth=2,constraints=1
choice generators:  thread=3 (signal=0,lock=1,sharedRef=0,threadApi=2,reschedule=0), data=0
heap:               new=70293134,released=50,maxLive=959,gcCycles=2
instructions:       1124686375
max memory:         520MB
loaded code:        classes=114,methods=2797

====================================================== search finished: 7/8/25, 5:16 PM

[Mahmoud-Khawaja]

Hello @Tom-Soucies ,

The issue I see here is that there are over 70 million heap objects with only three states, which is leading to state space explosion.

One suggestion is to try to eliminate threading where possible. Currently, there are three threads: Model.java, and its inner classes Model$Substracter and Model$Divider. If you're using thread.start(), consider replacing it with thread.run() (this will invoke the method directly without creating a new thread).

However, the main thing you need to focus on is limiting the search space and optimizing memory usage. For example, you can configure the .jpf file with the following settings:

search.depth_limit=25
vm.max_heap_size=4096m

I think these adjustments should help reduce the memory footprint and control the state explosion.

If threading is essential, you may share your code so we can see if there's an alternative approach.
You might also consider scaling up gradually. For example, start with:

2 states, 1 event, 0 variables, and no threading
Then move to:
2 states, 1 event, 1 variable
…and so on.

This approach can help you identify exactly where the state explosion begins and control complexity step by step.