lip6 / itstools Goto Github PK

I found a bug in the flatten function, more precisely in the part that simplifies constant variables.

Given two constants array a and b, the expression a[b[0]] in a property is replaced by a[x] (where x is the value of b[0]), but the array a is deleted.

Before flatten:

  typedef Boolean= 0..1 ;
  typedef T_Attacker= 0..0 ;
  typedef T_Item= 0..1 ;
  int _init = 0;
  array [1]T_Attacker.personal = (1 );
  array [1]T_Attacker.stolen = (-1 );
  array [2]Attacker_types = (0, -1 );
  transition B_take__1__T_Attacker__T_Item(T_Attacker $attacker, T_Item $item) [ _init == 1 && true ] {
    T_Attacker.stolen[ ( ( $attacker * 1 ) + Attacker_types[ 0 ] ) ] = ( ( $item * 2 ) + 1 )    ;
  }
  transition init [ _init == 0 ] {
    _init = 1    ;
    if (!( true) ) {
      abort ;
    }
  }
}
property "get"  [reachable] : 
  _init == 1 && T_Attacker.stolen[ ( ( 0 * 1 ) + Attacker_types[ 0 ] ) ] == T_Attacker.personal[ ( ( 0 * 1 ) + Attacker_types[ 0 ] ) ]
;

After flatten:

  /**    Dom:[0, 1] */
  int _init = 0;
  array [1]T_Attacker.stolen = (-1 );
  transition B_take__1__T_Attacker__T_Item_attacker0_item0 [ _init == 1 ] {
    T_Attacker.stolen[ 0 ] = 1    ;
  }
  transition B_take__1__T_Attacker__T_Item_attacker0_item1 [ _init == 1 ] {
    T_Attacker.stolen[ 0 ] = 3    ;
  }
  transition init [ _init == 0 ] {
    _init = 1    ;
  }
}
main null_inst ;
property "get"  [reachable] : 
  _init == 1 && T_Attacker.stolen[ 0 ] == T_Attacker.personal[ 0 ]

;

I wanted to transform a promela file into GAL, but I get the error
"Some files were not transformed due to errors (1 files): test_row: index=0, size=0".

What does index=0, size=0 mean? How can I fix it?

The promela file contains several new language features (for-loops, select statement). Maybe they cause the error? Unfortunately, the promela code is under NDA.

We at least need to be able to choose which tool will be run, without commenting formulas.

we would like to have a (property file + model) passed to Check call.

When a foreign formalism is used, we want to keep the property file across runs.

Options
a) we have a foreign property file, e.g. .q file for XTA, transform it as well
b) the user writes the props for the GAL target, hopefully the (re)generated model still fits it.We want to keep that file and reuse for subsequent runs.

This feature would ideally involve patching current issues with import mechanism across files, which is broken since Xtext 2.9 for us.

there is no real reason we could not use the parameters in the property specification, we having some kind of AndAll/OrAll (or forAll, forAny) quantifiers + bool expr over parameters would be nice

e.g. viking
typedef vik_t = 0..3;
property safe [reachable] : win==1 && forAll($vik : vik) { Soldier_state[$vik]==2 };

syntax to be discussed, but that forall is a boolean Expr.

I'm currently stuck because the code I'm working on depends on a version of GAL of mid of March and I haven't updated my installation at that time. (I have only an incompatible February version)
Now I wish to work on it, but can't because of the current major regression #9 .
Could you consider to deploy several versions of GAL/ITS so in case of trouble, we can at least retrieve the previous working version ?
Ideally, this would be coupled with a release process when the code is relatively stable.

Run as its model check only accepts .gal files

Add support for .xta, .dve, .pml, .net (Tina), .ndr (Tina), .xml (Romeo), .model (coloane), .pnml by leveraging existing transformations.

Description

The urgent channels of XTA (see https://www.it.uu.se/research/group/darts/papers/texts/new-tutorial.pdf page 6) do not seem to be supported, at least in the XTA editor.

How to reproduce

Open file:

urgent chan sys_2_o2_res, sys_2_o2_req, sys_1_o1_req;

process sys_e() {

state
    l_error,
    l_correct,
    l_s0,
    l_s1,
    l_s2;
init l_s0;
trans
    l_s0 -> l_s1 { sync sys_1_o1_req!;  },
    l_s0 -> l_error { sync sys_2_o2_req!;  },
    l_s1 -> l_s2 { sync sys_2_o2_req!;  },
    l_s2 -> l_correct { sync sys_2_o2_res?;  },
    l_correct -> l_correct {  },
    l_error -> l_error {  };
}

process sys_s() {
clock c_6884493603270001633, c__3232429354967973480;
state
    l_sNEW {c_6884493603270001633 <= 4},
    l_s0,
    l_s1 {c_6884493603270001633 <= 4},
    l_s2 {c__3232429354967973480 <= 5},
    l_s3;
init l_s0;
trans
    l_s1 -> l_sNEW { guard c_6884493603270001633 >= 2;  },
    l_s0 -> l_s1 { sync sys_1_o1_req?; assign c_6884493603270001633 = 0;  },
    l_sNEW -> l_s2 { sync sys_2_o2_req?; assign c__3232429354967973480 = 0;  },
    l_s2 -> l_s3 { guard c__3232429354967973480 >= 2; sync sys_2_o2_res!;  },
    l_s3 -> l_s3 {  };
}
Process_sys_e = sys_e();
Process_sys_s = sys_s();
system Process_sys_e, Process_sys_s;

With the newest version of gal 1.0.0.201804131302 (mid april 2018)
when trying to run its reach or to flatten a gal file (such as the one in attachment) we get a Null Pointer Exception

java.lang.NullPointerException
	at org.eclipse.emf.ecore.util.Switch.doSwitch(Switch.java:69)
	at fr.lip6.move.gal.instantiate.EventCopier.caseVariableReference(EventCopier.java:110)
	at fr.lip6.move.gal.instantiate.EventCopier.caseVariableReference(EventCopier.java:1)
	at fr.lip6.move.gal.util.GalSwitch.doSwitch(GalSwitch.java:305)
	at org.eclipse.emf.ecore.util.Switch.doSwitch(Switch.java:53)
	at org.eclipse.emf.ecore.util.Switch.doSwitch(Switch.java:69)
	at fr.lip6.move.gal.instantiate.EventCopier.caseAssignment(EventCopier.java:233)
	at fr.lip6.move.gal.instantiate.EventCopier.caseAssignment(EventCopier.java:1)
	at fr.lip6.move.gal.util.GalSwitch.doSwitch(GalSwitch.java:239)
	at org.eclipse.emf.ecore.util.Switch.doSwitch(Switch.java:53)
	at org.eclipse.emf.ecore.util.Switch.doSwitch(Switch.java:69)
	at fr.lip6.move.gal.instantiate.EventCopier.caseTransition(EventCopier.java:172)
	at fr.lip6.move.gal.instantiate.EventCopier.caseTransition(EventCopier.java:1)
	at fr.lip6.move.gal.util.GalSwitch.doSwitch(GalSwitch.java:186)
	at org.eclipse.emf.ecore.util.Switch.doSwitch(Switch.java:53)
	at org.eclipse.emf.ecore.util.Switch.doSwitch(Switch.java:69)
	at fr.lip6.move.gal.instantiate.Instantiator.instantiateParameters(Instantiator.java:817)
	at fr.lip6.move.gal.instantiate.Instantiator.instantiateParameters(Instantiator.java:303)
	at fr.lip6.move.gal.instantiate.GALRewriter.instantiateParameters(GALRewriter.java:62)
	at fr.lip6.move.gal.instantiate.GALRewriter.flatten(GALRewriter.java:17)
	at fr.lip6.move.gal.itstools.launch.CommandLineBuilder.buildCommand(CommandLineBuilder.java:62)
	at fr.lip6.move.gal.itstools.launch.ITSLaunchDelegate.launch(ITSLaunchDelegate.java:25)
	at org.eclipse.debug.internal.core.LaunchConfiguration.launch(LaunchConfiguration.java:885)
	at org.eclipse.debug.internal.core.LaunchConfiguration.launch(LaunchConfiguration.java:739)
	at org.eclipse.debug.internal.ui.DebugUIPlugin.buildAndLaunch(DebugUIPlugin.java:1039)
	at org.eclipse.debug.internal.ui.DebugUIPlugin$8.run(DebugUIPlugin.java:1256)
	at org.eclipse.core.internal.jobs.Worker.run(Worker.java:56)

MyBuilding_main_goal_reach.galparam.gal.txt

the previous version (march 2018) was working fine.

Hi,

I'm currently investigating the feasibility of using the GAL formalism in a side project of mine.

The current approach characterises a system's semantics in terms of the SMV formalism. This works pretty well but introduces unnecessary intermediate states that I can get rid of when using GAL instead -- in particular its fixpoint actions.

However, one feature of SMV that I cannot reproduce without jumping through hoops is the restriction of a system's state space by a given predicate -- called INVAR constraint in SMV.

My use case is that I want to check reachability of bad states B(X). However, I also have a static analysis that can quickly under-approximate the states from which B(X) cannot be reached. Therefore I would like to use this outcome (its negation) to constrain the search space, and avoid exploration of some parts that are known to never reach B(X).

I'm aware that I could do this manually with libITS, by restricting the state space after every action, but was wondering whether there is already an easy way to restrict the state space in GAL.

Hi,

First of all, thanks for all the efforts on providing these tools and their extensive documentation.

I am considering using GAL as a target language for my use case and I have been investigating what the generated GALs should look like. In this problem domain there are state variables whose value are dependent on the values of other variables in the state (I will refer to them as dependent variables). Thus, after (or at the end) of firing a transitions the variables that depend on variables that have been changed should be updated.

A dependency analysis can reveal which transitions require which dependent variables to be updated so that the code generation procedure can insert the code that updates the right variables at the end of each transition. For efficiency reasons this would be the right approach in the long run. However, initially I am considering generating the code for updating all dependent variables at the end of each transition.

Readability can be improved by generating the code for updating all dependent variables once, inside a labelled transition that is called at the end of every transition (essentially using it as a procedure). This works fine.

The problem is the initial state, in which the dependent variables should also be initialised properly. For obvious reasons, it is not possible to call the labelled transition after initialising all the state variables. For reasons less obvious to me, variables can only be initialised through expressions that do not refer to other variables. This is somewhat surprising to me because, if variables did depend on variables (and only variables), then it is possible to perform constant propagation and modify the initialisation of the dependent variables to a constant expression (and the system already appears to do constant propagation to simplify the program).

My problem thus boils down to having to perform the constant propagation on my side, before code generation. This is clearly not a show-stopper, but I though to write this message anyway because perhaps responses might clear some things up for me.
On the one hand I am curious as to way initialisation cannot involve references to other variables. On the other hand, I expect that the scenario I described, in which dependent values need to be updated after every transition, is very common, and perhaps some other solution is available that I have overseen.

Any insights would be very welcome.

Best,
Thomas

On a freshly installed linux (ubuntu 17.10)
when installing itstools via eclipse and running its-reach contained in fr.lip6.move.gal.itstools.binaries.

this run fails with the following error:

/home/dvojtise/eclipses/atsyra_studio_sdk_latest/plugins/fr.lip6.move.gal.itstools.binaries_1.0.0.201712050952/bin/its-reach-linux64: error while loading shared libraries: libgmpxx.so.4: cannot open shared object file: No such file or directory

apparently its-reach is compiled using dynamic libraries that are not part of default linux installation.

workaround : manually install libgmp

sudo apt-get install libgmp-dev

however, a better solution would be to statically include the lib

flags such as itness and -print-states cannot be passed from eclipse

Consider the following model:

GAL model {
int AA =0;
int BB =0;
transition aabb [ (AA < 6 ) ]
{ AA = AA+2 ;
BB = AA; }
}
main model;
property ltlaabb [ltl] : X (AA==BB) ;

Is it really intended that the execution of the transition "aabb" brings the system
from state (AA=0,BB=0) to state (AA=2,BB=4)?
(therefore making false property "ltlaabb")

Which kind of "sequential composition" is that?

Regards
Franco Mazzanti

Dear Team,
I am considering to use ITS-CTL, because it has support
for importing an explicit model (via ETF) and can produce counter-examples on ctl-properties.

So, I performed some 2 toy experiments: 'simpleexample' and 'otherexample': its.zip

'simpleexample' behaves fully as expected: 
-  the ETF model is imported successfully and
-  all the formulas received a verdict
-  all formulas have a trace, either a witness or a counterexample.

'otherexample' behaves not fully as expected: 
-  the ETF model is imported successfully and
-  all the formulas received a verdict
-  all formulas, but the last one,  have a trace ( either a witness or a counterexample)

• the last formula, AG(rip="false"), shows the following behavior:
• The verdict of the formula against the model is calculated and is as expected : FALSE.
• It fails on computing a witness: 'No transition found to progress in witness path construction. Something is wrong with the transition relation extraction.'
• Reports a Segmentation fault (core dumped) and the program halts.

Is there maybe a requirement that i missed in properly using its-ctl ? or is this unexpected behavior indeed tool-related? 

Kind regards
Carlo 
Student Ou.nl