Menu

#83 "error while running tool ..."

closed
5
2008-04-23
2008-03-31
Paul
No

When building the joined project, i get the following error message :
"error while running tool (automatic proof obligation manager)".

Discussion

  • Paul

    Paul - 2008-03-31

    project example

     
  • Nobody/Anonymous

    Logged In: NO

    Thanks to a steve_j_wright post (http://sourceforge.net/forum/forum.php?thread_id=1963966&forum_id=373711)
    I change the way rodin launches :
    "C:\Program Files\rodin 0.8.1\rodin.exe" -vm java.exe -vmargs -Xms600m -Xmx800m instead of
    "C:\Program Files\rodin 0.8.1\rodin.exe"

    (I have only a 1 GB for RAM and i will have to change the PC for enlarging RAM from now on !)

    Then the problem stops ! ;-)
    But the next refinements will probably remind me that problem...

     
  • Laurent Voisin

    Laurent Voisin - 2008-04-07
    • labels: --> 817327
    • milestone: 774588 --> 818778
    • assigned_to: nobody --> lvoisin
     
  • Laurent Voisin

    Laurent Voisin - 2008-04-07

    Logged In: YES
    user_id=1041912
    Originator: NO

    The machine produces 348 proof obligations. The PR file grows very large: e.g., 24 Mb for 112 discharged POs.

    The cause of the large PR file is the extensive use of forward rules and/or of ML.

    Need to see what can be done to make the file smaller.

     
  • Laurent Voisin

    Laurent Voisin - 2008-04-09
    • labels: 817327 --> Event-B Prover
    • milestone: 818778 -->
     
  • Laurent Voisin

    Laurent Voisin - 2008-04-09

    Logged In: YES
    user_id=1041912
    Originator: NO

    The root of the problem is memory usage. The marker reported is due to an OutOfMemory exception while auto-proving the machine.

    The large memory consumption is due to the format in which proofs are stored in the database. The current format is too detailed for proper handling of a large set of POs. We currently have a six-fold increase between the PR file size and the core memory used to represent it. For instance, a PR file of 27 Mb uses 165 Mb of heap space.

    Another direction is to prune the forward inferences which are present but unused in a proof. Here, there are a lot of axioms which are not normalized and produce forward inferences for normalizing them, although these axioms are seldom relevant to the proof at hand. Such pruning of unused forward steps would be a giant step towards smaller proof files.

    Changed the nature of this entry to "feature request".

     
  • Laurent Voisin

    Laurent Voisin - 2008-04-23

    Context with normalized predicates

     
  • Laurent Voisin

    Laurent Voisin - 2008-04-23
    • status: open --> closed
     
  • Laurent Voisin

    Laurent Voisin - 2008-04-23

    Logged In: YES
    user_id=1041912
    Originator: NO

    If you modify the context, so that all predicates "x ≠ y" are rewritten as "¬x = y" (see attached file), then the auto-prover can be run in less than 64 Mb. The resulting PR file is about 1.2 Mb. I consider this acceptable.

    Consequently, the UI must be changed so that it generates normalized predicates for enumerated sets (see FR #1949585). A complement approach would be to trim down proofs when committing them, by removing useless forward rules (see FR#1949582).
    File Added: c00.buc

     

Log in to post a comment.