Hi,

So the constraint on not having initial expressions depending on variables could be relaxed a bit, provided they are cycle free, I was kind of afraid of malformed models a inits to b that inits to foo(a), the goal is to rewrite this syntactic sugar (e.g. parameters...) to have an initial state where all variables are bound. Bref supporting that is not a difficult feature to add I believe.

An alternative that some users have used in the past is to have a pre-initial state (add a init=0 var), and add a special initialization transition [init =0] { init= 1; // do init } and guard all other transitions by "init==1".
That also allows if you "call" some labels to "initialize" in several states rather than a single initial state. The command line tools then have an "--init-gadget" flag, that skips to immediate successors of the "initial" gal state. As you can see this feature is mostly meant for multiple initial states (e.g. an initial set of situations, satisfying some boolean constraints) , so not quite your use case.

Concerning dependent updates, yes it is a relatively common scenario, but there is no "one size catches all" I think. I think starting as you are doing is ok, then improving your generator at some point to add a "update" transition per primary variable, and only calling updates for variables written to in the transition (or basically adding a self."var_update"; after any var=...XXX... ; assignment).

Another alternative could be to get rid of these evil/redundant variables, whose value can be deduced from primaries, if the dependent updates are deterministic/memory free, i.e. in any state, value of dependent DV is computed as foo(primary1,primary...), just use foo(p1,p2...) instead of your dependent variable. This is probably the best option for the symbolic DD solution engine, which does not much appreciate having variables that are so strongly dependent on one another.

Concerning implementing this kind of things, there is plenty of support for it in the ITSTool library, e.g. computation of support for arbitrary GAL statements, support for duplicating things, constant propagations etc... but this implies you're using Java/EMF which might not be the case. If you are using that technology chain, I can point you to a few primitives / code samples that do similar things to what you want.

Best regards
ytm

note : if solution "get rid of evil" fits your use case, actually maybe defining derived variables as an expression of normal or derived variables (cycle free) could be added as syntactic sugar, so that these variables can still be used in logic and tests, just a compact form for their expansion (sort of inlining)

something like :
derived int dvar= (var1 + var2 >0) ;
and use dvar in the rest of the code

This expansion would come early, so that the rest of the tool is not updated, just syntactic sugar.

Many thanks for your detailed response!

Your suggestion to inline the expressions is very helpful, and is a good option for my use case.
I prefer to maintain a close connection to the source program, so your suggestion for a layer of syntactic sugar is spot on!

note : if solution "get rid of evil" fits your use case, actually maybe defining derived variables as an expression of normal or derived variables (cycle free) could be added as syntactic sugar, so that these variables can still be used in logic and tests, just a compact form for their expansion (sort of inlining)

something like :
derived int dvar= (var1 + var2 >0) ;
and use dvar in the rest of the code

This expansion would come early, so that the rest of the tool is not updated, just syntactic sugar.

Using the let keyword would perhaps be more suggestive of the declarative nature of this construct, as in:

let dvar = (var1 + var2 > 0);

or perhaps even more suggestive is to use alias:

alias dvar = (var1 + var2 > 0);

So the constraint on not having initial expressions depending on variables could be relaxed a bit, provided they are cycle free

A natural restriction to avoid cycles would be to allow only references to variables declared "above" the current initialisation.

ok, the constraint on not referring to variables below is a reasonable one, pretty natural, a lot of languages have that. I can try to implement it like that rather than reporting cycles as an error, report forward references is easier.

Adding a keyword, and the corresponding expansion in my tool is not difficult, traceability will be a bit degraded as the command line stuff won't know about them, but maybe we can post process the outputs to reconstruct derived variables values in traces if that becomes problematic.

let declares true variables in a lot of languages with that keyword, alias has less connotations, maybe it's a better keyword, I can't think of a really similar concept in other languages where there would be a well known keyword, alias is pretty explicit.

Hi, ok here is a beta version of the feature;

gal TestAlias {
	
	int x=0;
	int y=1;
	alias xp = (x >0 || y > 0);
	
	transition t [xp == 1] {
		x=1;
		y=0;
	}
	
}

now works as we have discussed.
I have not updated the fact variables cannot depend on variables yet.
New version will be up in roughly 1/2 hour, just restart eclipse and update ITS-tools to get the feature.

Terrific! Thanks.

With these feature it should not be necessary for me to initialise variables based on other variables.

I will let you know how I get on once I start generating GALs.

I updated my test program to use the alias keyword to see whether all the properties still succeeded.
Unfortunately, the property with an alias in it did not succeed.

property prop [ctl] : EF(var == 1);

Here var has been defined as an alias:

alias var = (x + y > 0);

The output of its-ctl gives:

original formula: FALSE
=> equivalent forward existential formula: [(Init * FALSE)] != FALSE

This suggests to me that var == 1 is rewritten by constant propagation so that var is replaced with 0 based on the initial values of x and y. However, I expected the value of var to be the result of evaluating its expression in each of the considered states.

When I do the inlining, the result is as I expect:

property prop [ctl] : EF((x + y > 0) == 1);

Formula is TRUE !

Ok, another attempt, with some support for properties, sorry I missed that,

gal TestAlias {
	int x=0;
	int y=1;
	alias xp = (x >0 || y > 0);
	
	transition t [xp == 1] {
		x=1;
		y=0;
	}
}

composite Comp {
	TestAlias a;
	TestAlias b;
		
}

main Comp;

property pA [reachable] : a:xp == 2 && b:xp == 0;

now works, there was a bit more work involved for requalifying variables in properties like in this example. Same as last time give it roughly 30 minutes to build an deploy.

Resulting image after degeneralization is the expected :

gal TestAlias_flat{
  /**    Dom:[0, 1] */
  int x = 0;
  /**    Dom:[0, 1] */
  int y = 1;
  transition t [ (x > 0 || y > 0) == 1 ] {
    x = 1    ;
    y = 0    ;
  }
}
composite Comp_flat {
  TestAlias_flat a;
  TestAlias_flat b;
}
main Comp_flat ;

• property

property pA [reachable] : ((((a.x>0)||(a.y>0))==2)&&(((b.x>0)||(b.y>0))==0))

meh, looking at it, the tool should conclude false immediately, a bool is in range 0..1, the && simplifies the rest, there is room for syntactic simplification.

I'll need to document the keyword and add an example on the gal description page, i.e. edit https://github.com/lip6/ITSTools-web/blob/master/galbasics.md and add an example. If you have the time to propose a paragraph and/or a small didactic/relevant example using the new keyword that would be really appreciated (otherwise don't worry about it I'll build on the example in this thread)
.