K-user mailing list

[Gurvan Le Guernic <gleguern AT gmail.com>]

   Hi,

 Sorry for the previous email that was erroneously sent before being finished.

 My general problem is the following: I have a rule that applies (a configuration transformation) if the current configuration matches (sub-configuration) pattern A and pattern B. I want to write a rule that applies if the current configuration matches pattern A and DOES NOT match pattern B.

 I am specifying a language containing a command "step" that triggers (through an event) a transition in an automaton if the transition is allowed and generates an error if the transition is not allowed.

 My configuration contains the following fragment for the definition of kind of automata:
  <automatonDefs color="gray"> // If not present: [Error] Internal: Uncaught exception thrown of type AssertionError.
    <automatonDef color="gray" multiplicity="*">
      <automatonName color="gray"> "":String </automatonName>
      <initialState color="gray"> "":AStateId </initialState>
      <transition color="gray" multiplicity="*">
        <from color="gray"> "":AStateId </from>
        <evt color="gray"> "":AEvtId </evt>
        <to color="gray"> "":AStateId </to>
      </transition>
    </automatonDef>
  </automatonDefs>
 the kind and current states of the automata are stored in Maps:
  <env color="green">
    <vars color="green"> .Map </vars>
    <automata color="green"> .Map </automata>
  </env>

 The rule for step when the transition applies is the following (#Id is an identifier of automaton):
  rule
    <k> step( # X:Id , E:AEvtId , _:Filter) => . ... </k>
    <automata> ... X |-> N ... </automata>
    <automatonDef> ...
      <automatonName> N </automatonName>
      <transition>
        <from> F </from>
    <evt> E </evt>
    <to> T </to>
      </transition>
    ... </automatonDef>
    <vars> ... X |-> (F => T) ... </vars>

 I would like to write a rule that says roughly:
  rule
    <k> step( # X:Id , E:AEvtId , F:Filter) => F ... </k>
    <automata> ... X |-> N ... </automata>
    <vars> ... X |-> F ... </vars>
    "and there exists no T such that:"
    <automatonDef> ...
      <automatonName> N </automatonName>
      <transition>
        <from> F </from>
        <evt> E </evt>
        <to> T </to>
      </transition>
    ... </automatonDef>

 Is it possible to express such "vacuous" mapping condition on the configuration ? I guess I could solve my problem by saving in duplicate possible transitions in a Map and using something similar to "when notBool (X in keys(Rho))", but it seems redundant and not elegant.

   Sincerely,
   Gurvan Le Guernic