Sequential composition of assignments?? about itstools

[francomazzanti]

The problem occurs only when running itstools from the inside of Eclipse (macOS version).
Re-executing in the terminal the same command that appears on the console:
"Eclipse.app/Contents/Eclipse/plugins/fr.lip6.move.gal.itstools.binaries_1.0.0.201806011319/bin/its-lts-Darwin -i new_file.gal -t CGAL ... ... " produces the normally expected results !!!

[francomazzanti]

The problems is caused by the fact that the original source model:
gal model{
int AA = 0;
int BB = 0;
transition aabb [ AA < 6 ] {
AA = ( AA + 2 ) ;
BB = AA ;
}
}
main model;

is wrongly (?!?!) traslated by eclipse inside the private "work" directory as:

gal model_flat{
int AA = 0;
int BB = 0;
transition aabb [ AA< 6 ] {
AA = ( AA + 2 ) ;
BB = ( AA + 2 ) ;
}
}
main model_flat ;

[yanntm]

Hi,
Sorry this looks like a bug or regression in the toolchain. I'll track the problem and patch it tomorrow. I'll post here when it's fixed.

[yanntm]

ok I've tracked it down,

ITSTools/fr.lip6.move.gal/src/fr/lip6/move/gal/support/SupportAnalyzer.java

Lines 278 to 290 in 3beb301

	* This function attempts to imporve commutativity of statements (assignments).
	* The rationale is thus :
	* s1 :a = x;
	* s2 :b = a;
	* We have s1 < s2, since write(s1) inter read(s2) non empty. But, if a is only assigned a value once, we could equivalently write
	* s1 :a = x;
	* s2 :b = x;
	* and have s1 <> s2 (commutative). The trick is that between s1 and s2, no variable read in x can written to.
	* x is an arbitrary expression.
	* This function works pretty well on some very specific patterns, but is a bit weak overall.
	* TODO : Not sure it handles "if" statements gracefully.
	* @param spec the spec whose action we are going to "improve" in place
	*/

this rewriting is missing on the fact that "x" depends on A.

[yanntm]

so line 286 should read : x is arbitrary but depends neither on A nor on B.

[yanntm]

So this should fix your problem if you update to the latest version (help-> check for updates) .

Thank you for reporting this problem in such audible fashion, please ask if you find any other issues or have feature requests/workflows that could be improved. LTL counter-examples are pretty tricky to interpret right now for instance.

As a side note, you might like to use : Ctrl-Shift-F shortcut to "Source->Format" to indent your gal files (it's not perfect but it's decent).