Slow execution speed for its command line tool

[lovis-hagemeyer]

Hi,

I am using the its command line tool and noticed that the tool needs several seconds even for very simple GAL systems. I have the following GAL file:

test_GAL.gal:

gal TestSystem {
  int x = 0;
  
  transition testTransition [x == 0] {
    x = 1;
  }
}

property formula[ctl] : EF(x == 1);

When I measure the execution time with time ./fr.lip6.move.gal.itscl.product-linux.gtk.x86_64/its-tools -ctl -i ./test_GAL.gal, I get the following output:

log4j:WARN No appenders could be found for logger (org.eclipse.xtext.parser.antlr.AbstractInternalAntlrParser).
log4j:WARN Please initialize the log4j system properly.
log4j:WARN See http://logging.apache.org/log4j/1.2/faq.html#noconfig for more info.
Successfully read input file : ./test_GAL.gal in -2795 ms.
Nov 12, 2024 3:07:25 PM fr.lip6.move.gal.instantiate.DomainAnalyzer computeVariableDomains
INFO: Found a total of 1 fixed domain variables (out of 1 variables) in GAL type TestSystem
Nov 12, 2024 3:07:25 PM fr.lip6.move.gal.instantiate.DomainAnalyzer computeVariableDomains
INFO: Found a total of 1 fixed domain variables (out of 1 variables) in GAL type TestSystem_flat
Nov 12, 2024 3:07:25 PM fr.lip6.move.gal.instantiate.GALRewriter flatten
INFO: Flatten gal took : 108 ms
Simplifications done in -112 ms.
Nov 12, 2024 3:07:25 PM fr.lip6.move.serialization.SerializationUtil systemToFile
INFO: Time to serialize gal into <path/to>/./work/test_GAL.gal : 14 ms
Nov 12, 2024 3:07:25 PM fr.lip6.move.serialization.SerializationUtil serializePropertiesForITSCTLTools
INFO: Time to serialize properties into<path/to>/./work/test_GAL.ctl : 3 ms
Built GAL and property files in -46 ms.
its-ctl command run as :

<path/to>/fr.lip6.move.gal.itscl.product-linux.gtk.x86_64/plugins/fr.lip6.move.gal.itstools.binaries_1.0.0.202407041249/bin/its-ctl-linux64  --gc-threshold  2000000  --quiet  -i <path/to>/./work/test_GAL.gal  -t  CGAL  -ctl  <path/to>/./work/test_GAL.ctl  
No direction supplied, using forward translation only.
Parsed 1 CTL formulae.
Model ,|S| ,Time ,Mem(kb) ,fin. SDD ,fin. DDD ,peak SDD ,peak DDD ,SDD Hom ,SDD cache peak ,DDD Hom ,DDD cachepeak ,SHom cache
reachable,2,0.003453,3200,2,2,5,6,6,0,5,4,0


Converting to forward existential form...Done !
original formula: EF((x==1))
=> equivalent forward existential formula: [(FwdU(Init,TRUE) * (x==1))] != FALSE
(forward)formula 0,1,0.005133,3456,1,0,6,6,8,1,8,4,1
Formula is TRUE !

 *************************************** 


real    0m6.136s
user    0m14.135s
sys     0m0.676s

So six seconds for a very simple GAL file. More complex GAL systems lead to roughly the same execution time, so this seems to be some constant overhead.
I want to test several hundred simple GAL systems using a script, so the delay makes that really impractical. Is there a way to avoid this?

Kind Regards
Lovis

[yanntm]

Hi,

Sorry I missed your mail/issue report,

The response is "no not really", we unfortunately drag a nasty dependency to EMF, a component of Eclipse, and startup time is a nasty few seconds.

It used to be less, but I think some of the platform components is now running some kind of useless check or validation of some sort. I have not been able to diagnose and remove it.

I apologize for the issue; it's as you noted a constant startup time penalty coming from the framework we rely on.

Depending on what features of GAL you use, you could go for the back end C++ tool ; but it understands a subset of the language and e.g. properties have a particular syntax that is not so comfortable. Still if you generate the examples it's feasible to target the format of the C++ tools, that pay no start cost at all.

You do lose some of the static simplifications that could occur, and the format is less user-friendly among other limits.

Another option could be that I add a batch flag where you could pass your target files in one invocation, that is pretty easy to do. At least you'd get a single startup penalty for a bunch of files.

[lovis-hagemeyer]

No problem, sometimes things just slip under the radar.

Using the backend C++ tool unfortunately is not really an option, but a batch flag would be great!