Add predicates/properties

[fredher]

TChecker currently check if some label is reachable. Properties would extend labels by allowing more general properties like "P1.l1 && 1 <= i <= 5 && x-y <= 6". Needs:

• parse properties from string (requires to extend expressions to allow labels as well as locations like P1.l1)
• compile the resulting expression into bytecode
• evaluate the bytecode on a state (evaluation depends on the state, as for instance in "x[2*i] <= a-b")

[fredher]

Interface with Spot:

• spot yields a list of atomic propositions ,ex: P.l, i<10,.etc
• Tchecker should provide the truth value of each atomic proposition (a function to evaluate each of them in spot, or a bitvector, or,...)

[fredher]

Atomic propositions on transitions would be a nice additions. What should we allow:

• predicates on pre/post states, ex: P.l1 & (P.l2)' ???
• predicates on events ex: P1.a || P2.b ???

[fredher]

We want:

• atomic propositions on states written on process locations and integer variables, ex: P1.l, x<3,...
• atomic propositions on transitions written on process events, ex: P1.a, P2.b,...
  We need to:
• determine if an AP is a state or a transition AP
• evaluate an AP (or a set of APs) on a state or a transition