Yann Thierry-Mieg

The code is non intrusive w.r.t. to the existing code structure so I hope that helps the PR go through. The only thing I'm not really sure about is that...

Thanks for the link visible from closed issue Z3Prover/z3#4713. , I guess I'll go with 4.8.7 too, I have the same kind of errors cropping up, it was hard to...

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...

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...

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...

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...

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...

Resulting image after degeneralization is the expected : ``` gal TestAlias_flat{ /** Dom:[0, 1] */ int x = 0; /** Dom:[0, 1] */ int y = 1; transition t [...

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...