Code review comment for lp:~tapaal-dist-ctl/verifypn/arithmeticExpressions

Revision history for this message
Jiri Srba (srba) wrote :

I can see some problems when parsing the expressions.

A query in the GUI is:

EF N.P0 * N.P1 + N.P2 * N.P2 - N.P4 = 0

and your engine prints it as:

Query before reduction: AG (((P0 + P1) * ((P2 + P2) - P4)) == 0)

but the XML query output seems correct:

 <exists-path>
        <finally>
          <integer-eq>
            <integer-sum>
              <integer-product>
                <tokens-count>
                  <place>P0</place>
                </tokens-count>
                <tokens-count>
                  <place>P1</place>
                </tokens-count>
              </integer-product>
              <integer-difference>
                <integer-product>
                  <tokens-count>
                    <place>P2</place>
                  </tokens-count>
                  <tokens-count>
                    <place>P2</place>
                  </tokens-count>
                </integer-product>
                <tokens-count>
                  <place>P4</place>
                </tokens-count>
              </integer-difference>
            </integer-sum>
            <integer-constant>0</integer-constant>
          </integer-eq>
        </finally>
      </exists-path>

review: Needs Fixing

« Back to merge proposal