Loading ...
Sorry, an error occurred while loading the content.
 

Re: [UPPAAL] Strange behaviour of time

Expand Messages
  • Daniel Karlsson
    The example I provided before now works in the new version of UPPAAL, which is great. However, that example resulted from a more complicated example which I
    Message 1 of 4 , Feb 20, 2002
      The example I provided before now works in the new version of UPPAAL, which is
      great. However, that example resulted from a more complicated example which I
      reduced in order to show the essence of the problem. I will below provide a less
      reduced example which does not work even in the new version. I would like some
      comment on whether this also is due to a bug or due to my misunderstanding.

      Consider two locations, p and q, and a clock c. p is the initial location. p
      also has the invariant "c<=3". Add a transition from p to q. Add a guard to this
      transition: "c>=2, c<=3". Let's call this system P.

      The verifier agrees that the following property is true: "A<> P.q". However, it
      claims that "A<> (P.q and c>=2)" is false. Isn't this basically the same thing
      as my previous example?

      Let's also look at two other similar properties. The verifier agrees that "P.p
      --> P.q" is true. But it disagrees with me that "P.p --> (P.q and c>=2)" is
      true.

      If I replace "c>=2" in the above properties with "c<=3", I get the expected
      answer that the properties are satisfied.

      /Daniel Karlsson
    • Gerd Behrmann
      Dear Daniel Karlsson, You are right. This is a bug, although it is not the same bug - this time it is a problem with the deadlock check integrated into the
      Message 2 of 4 , Feb 25, 2002
        Dear Daniel Karlsson,

        You are right. This is a bug, although it is not the same bug - this
        time it is a problem with the deadlock check integrated into the
        liveness checker. It will be fixed as soon as possible.

        Thanks for reporting this.

        Regards,

        /gerd

        On Wed, 2002-02-20 at 17:59, Daniel Karlsson wrote:
        >
        > The example I provided before now works in the new version of UPPAAL, which is
        > great. However, that example resulted from a more complicated example which I
        > reduced in order to show the essence of the problem. I will below provide a less
        > reduced example which does not work even in the new version. I would like some
        > comment on whether this also is due to a bug or due to my misunderstanding.
        >
        > Consider two locations, p and q, and a clock c. p is the initial location. p
        > also has the invariant "c<=3". Add a transition from p to q. Add a guard to this
        > transition: "c>=2, c<=3". Let's call this system P.
        >
        > The verifier agrees that the following property is true: "A<> P.q". However, it
        > claims that "A<> (P.q and c>=2)" is false. Isn't this basically the same thing
        > as my previous example?
        >
        > Let's also look at two other similar properties. The verifier agrees that "P.p
        > --> P.q" is true. But it disagrees with me that "P.p --> (P.q and c>=2)" is
        > true.
        >
        > If I replace "c>=2" in the above properties with "c<=3", I get the expected
        > answer that the properties are satisfied.
        >
        > /Daniel Karlsson
        >
        >
        >
        >
        > To unsubscribe from this group, send an email to:
        > uppaal-unsubscribe@egroups.com
        >
        >
        >
        > Your use of Yahoo! Groups is subject to http://docs.yahoo.com/info/terms/
        >
      Your message has been successfully submitted and would be delivered to recipients shortly.