1. 22 Oct, 2015 2 commits
  2. 09 Sep, 2015 1 commit
  3. 07 Sep, 2015 1 commit
    • David Hauzar's avatar
      Different handling of postconditions in counterexamples. · 7ef0629a
      David Hauzar authored
      Postconditions for that variables mentioned in these postconditions
      should be in counterexample are now marked with label "model_vc_post".
      
      Variables corresponding to return values are no longer handled by
      transformation intro_vc_vars_counterexmp. They must have location
      of the corresponding postcondition, label "model" or "model_trace", and
      label of the form "model_trace:name@result". Generartion of these labels
      to variables corresponding to return values created in WP is for future
      work.
      7ef0629a
  4. 05 Aug, 2015 1 commit
    • David Hauzar's avatar
      Introducting constants with model labels for variables in the term · 0b53e050
      David Hauzar authored
      triggering VC.
      
      - Transformation intro_vc_vars_counterexamp introduces new constant with
      model labels for every variable in the term that trigger VC and axiom
      that this constant is equal to the variable, finds the position of the
      term that trigger VC, and saves this position in meta (for smtv2
      printer).
      
      - Transformation prepare_for_counterexmp additionally performs the
      transformation intro_vc_vars_counterexamp
      
      - smtv2 printer no longer collects the location of the term that
      triggers VC and does not collect variables in this term in a special
      way. Note that this functionality was not yet completely removed from
      the printer. It will be done so after the transformation
      intro_vc_vars_counterexmp will be tested.
      
      The rationale:
      Variables that should be displayed in counterexample are marked
      by model labels ("model", "model_projected", "model_trace:*").
      
      Variables inside the term that triggers VC should be displayed in
      counterexample for that VC. However, many VCs (tasks) can be generated
      for  a signle *.mlw file and only variables in the term that trigger
      the VC (task) that is currently proven should be displayed. That means
      that the process of selecting variables inside the term that triggers
      VC for counterexample must be done while processing the task. It is
      done by transformation intro_vc_vars_counterexmp. This means that smtv2
      printer no longer has to find the position of the term that triggers
      VC and no longer has to collect variables in this term in a special
      way.
      0b53e050