[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: [PVS-Help] Unit composition in PVS



Hi Ben,

Both of these problems are bugs.  The infinite loop is due to a bug
that was triggered by the subtype-tcc strategy on certain kinds of
arithmetic formulas.

The second bug was due to the code that tries to typecheck only as much of
the theory as necessary; I think I've fixed it, but this is harder to
test.

Could you try out the following patch file, and see if it helps?
Just create a "pvs-patches" subdirectory in your PVS installation if there
isn't one there already, and put it in there.  It should load the next
time you start PVS.

Thanks,
Sam

(in-package :pvs)

(defun assert-sform (sform &optional rewrite-flag simplifiable?)
  (let ((*assert-typepreds* nil)
	(*auto-rewrite-depth* 0)
	(*use-rationals* t))
    (multiple-value-bind (signal sform)
	(assert-sform* sform rewrite-flag simplifiable?)
      (cond ((eq signal '!)(values signal sform))
	    ((and (null *ignore-typepreds?*)
		  (or (eq signal '?) *assert-typepreds*))
	     ;; For some formulas (e.g., large, with lots of arithmetic)
	     ;; the *assert-typepreds* can get very large, and take
	     ;; a long time to process; hence the *ignore-typepreds?* flag.
	     (let ((newsig (process-assert-typepreds *assert-typepreds* signal)))
	       ;; should be signal, but fails for the example
	       ;; from Cesar 2012-12-10/aaaa.pvs
	       (values newsig sform)))
	    (t (values signal sform))))))

(defun process-assert-typepreds (assert-typepreds signal)
  (if (null assert-typepreds)
      signal
      (let* ((fmla (car assert-typepreds))
	     (sign (not (negation? fmla)))
	     (body (if sign fmla (args1 fmla))))
	(if (not (connective-occurs? body))
	    (let* ((res (call-process fmla *dp-state*)))
	      (cond ((true-p res)
		     (process-assert-typepreds (cdr assert-typepreds) signal))
		    ((false-p res)
		     '!)
		    ((and (consp res)
			  (not (update-or-connective-occurs? body)))
		     (loop for x in res
			do (push x *process-output*))
		     (process-assert-typepreds (cdr assert-typepreds) signal))
		    (t (process-assert-typepreds (cdr assert-typepreds) '?))))
	    (process-assert-typepreds (cdr assert-typepreds) signal)))))

(defmethod copy-lex-upto (diff (oth module) (nth module))
  (cond ((memq (car diff) (formals oth))
	 (assert (or (null (cdr diff)) (memq (cdr diff) (formals nth))))
	 (copy-lex-decls (ldiff (formals oth) (memq (car diff) (formals oth)))
			 (ldiff (formals nth) (memq (cdr diff) (formals nth)))))
	((memq (car diff) (assuming oth))
	 (assert (or (null (cdr diff)) (memq (cdr diff) (assuming nth))))
	 (copy-lex-decls (formals oth) (formals nth))
	 (copy-lex-decls (ldiff (assuming oth) (memq (car diff) (assuming oth)))
			 (ldiff (assuming nth) (memq (cdr diff) (assuming nth)))))
	(t
	 (assert (memq (car diff) (theory oth)))
	 (assert (or (null (cdr diff)) (memq (cdr diff) (theory nth))))
	 (copy-lex-decls (formals oth) (formals nth))
	 (copy-lex-decls (assuming oth) (assuming nth))
	 (copy-lex-decls (ldiff (theory oth) (memq (car diff) (theory oth)))
			 (ldiff (theory nth) (memq (cdr diff) (theory nth)))))))

(defun typecheck-decl (decl)
  ;; This check is needed because typechecking an importing may remove
  ;; declarations from the current theory, but the decls list to
  ;; typecheck-decls will not be affected, and TCCs may be accidentally
  ;; added.
  (when (or (symbolp (generated-by decl))
	    (and (declaration? (generated-by decl))
		 (typechecked? (generated-by decl))))
    (if (and (typechecked? decl)
	     (not (typep decl '(or theory-abbreviation-decl
				   conversion-decl auto-rewrite-decl ;;mod-decl
				   judgement))))
	(if (mod-decl? decl)
	    (dolist (d (generated decl))
	      (if (importing? d)
		  (typecheck-using* (get-theory (theory-name d)) (theory-name d))
		  (let ((dhash (current-declarations-hash)))
		    (dolist (id (id-suffixes (id d)))
		      (pushnew d (get-lhash id dhash) :test #'eq)))))
	    (progn
	      (mapc #'(lambda (d)
			(let ((*insert-add-decl* t))
			  (add-decl d nil)
			  (when (tcc? d) (push d *tccdecls*))))
		    (generated decl))
	      (regenerate-xref decl)))
	(unwind-protect
	    (progn
	      (reset-beta-cache)
	      (assert (typep (current-theory) '(or module recursive-type)))
	      (setf (module decl) (current-theory))
	      (assert (module decl))
	      (tcdebug "~%    Typechecking ~a" decl)
	      (let ((stime (get-internal-real-time)))
		(typecheck* decl nil nil nil)
		(setf (typecheck-time decl) (realtime-since stime))
		(tcdebug " - ~d msec" (typecheck-time decl)))
	      (setf (typechecked? decl) t)
	      (remove-pseudo-normalize-freevar-entries))
	  (unless (or *loading-prelude*
		      (typechecked? decl))
	    (cleanup-typecheck-decls decl))))
    (put-decl decl)))

Ben Hocking <ben.hocking@xxxxxxxxxxxxxxxxxxxxxxx> wrote:

> Hi all,
> 
> While I have had much success since Sam helped me to understand what I was doing wrong previously, I’m now running into two issues in the attached code:
> 
> 
> First, and easiest to reproduce, is what appears to be some sort of non-ending loop. In the attached example, the theory siso_test as-is can be proven with 15 TCCs. However, if you restore the first line in valve parameters:
>   valve_max_flow_rate: posvolume_per_time = 0.1 * m^3 / s
> it apparently takes forever to finish. (Possibly not forever, but I’ve seen no evidence that it’s doing anything but garbage collecting.) I’ve tried this in a variety of settings, and the result is fairly consistent. Let me know if you’re unable to recreate.
> 
> Secondly, it seems that I’m needing to use “::real” in many places where it should not be necessary, and where adding it in similar places breaks the specification. For example, consider the following line from lengths.pvs:
>   length_pred_ax: AXIOM length_pred(0::real) AND length_pred(0 * m) AND length_pred(m)
> 
> If I remove the ::real, I get the message:
>   Expecting an expression
>   No resolution for length_pred with arguments of possible types:
>     0 : reals.real
> 
> However, if I now add the following line above it:
>   f, g:      VAR real
> the ::real is not needed in the length_pred_ax line.
> 
> In fact, if I add it back, I now get the message:
>   Expecting an expression
>   No resolution for length_pred with arguments of possible types:
>     0:: real : reals.real
> 
> Note that these results seem to have a bit of Heisenberg uncertainty involved, so you might have to try some variations on this to see it.
> 
> Thank you,
> Ben Hocking
> ben.hocking@xxxxxxxxxxxxxxxxxxxxxxx
> 
> 
> > On Apr 28, 2015, at 3:55 PM, Ben Hocking <ben.hocking@xxxxxxxxxxxxxxxxxxxxxxx> wrote:
> > 
> > Excellent, thank you very much.
> > 
> > I had originally attempted to allow complex lengths, but decided to back away from that for now, so just changing number to real works for me.
> > 
> > Best Regards,
> > Ben Hocking
> > ben.hocking@xxxxxxxxxxxxxxxxxxxxxxx
> > 
> > 
> > 
> > 
> >> On Apr 28, 2015, at 3:52 PM, Sam Owre <owre@xxxxxxxxxxx> wrote:
> >> 
> >> Hi Ben,
> >> 
> >> It turns out there are two definitions for length_pred.  One is
> >> automatically generated from the declaration
> >> 
> >> length: NONEMPTY_TYPE FROM real
> >> 
> >> which generates (run "M-x ppe" to see this)
> >> 
> >> length_pred: [real -> boolean]
> >> 
> >> Then you define another one over numbers.  Removing your definition causes
> >> problems with the definition
> >> 
> >> length?(n: number): bool =
> >>   number_field_pred(n) and real_pred(n) AND length_pred(n)
> >> 
> >> but this can be fixed using coercions, i.e., "length_pred(n::real)"
> >> 
> >> With these changes I had no problem discharging the TCCs.
> >> 
> >> An alternative may be to define your length_pred over number to be equal
> >> to the other length_pred when restricted to real, but you can still see
> >> sequents that look like they should be trivial, but require a definition
> >> expansion.
> >> 
> >> I'm going to look into improving show-expanded-sequent so it makes this
> >> clearer.
> >> 
> >> Regards,
> >> Sam
> >> 
> >> Ben Hocking <ben.hocking@xxxxxxxxxxxxxxxxxxxxxxx> wrote:
> >> 
> >>> Hi Sam,
> >>> 
> >>> Got back to this after working on something else for a while, when I used the ‘C-u M-x show-expanded-sequent’ command, I got the following:
> >>> ===================================
> >>> length_plus_length_is_length :
> >>> 
> >>> {-1}  length_pred((number_fields.+)(x, y))
> >>> |-------
> >>> {1}   length_pred((number_fields.+)(x, y))
> >>> ===================================
> >>> 
> >>> As far as I can tell, {-1} should imply {1} fairly cleanly. Neither ‘(assert)’ nor even ‘(grind)’ resolve this, but possibly the output from ‘(grind)’ is useful:
> >>> ===================================
> >>> The following errors occurred within the strategy:
> >>> 
> >>> Couldn't find a suitable quantified formula.
> >>> 
> >>> No suitable (+ve FORALL/-ve EXISTS) quantified expression found.
> >>> 
> >>> No change on: (grind)
> >>> length_plus_length_is_length :
> >>> 
> >>> [-1]  length_pred(x + y)
> >>> |-------
> >>> [1]   length_pred(x + y)
> >>> ===================================
> >>> 
> >>> The proof (from show-proof) is simply:
> >>> ("" (skeep) (lemma "closed_plus" ("x" "x" "y" "y")) (postpone))
> >>> 
> >>> Where the judgment being proven is:
> >>> length_plus_length_is_length:  JUDGEMENT +(x, y)   HAS_TYPE length
> >>> 
> >>> And the axiom closed_plus is:
> >>> closed_plus:    AXIOM length_pred(x + y) 
> >>> 
> >>> And the definition for x, y is:
> >>> x, y: VAR length
> >>> 
> >>> Best Regards,
> >>> Ben Hocking
> >>> ben.hocking@xxxxxxxxxxxxxxxxxxxxxxx
> >>> 
> >>> 
> >>> 
> >>> 
> >>>> On Apr 23, 2015, at 6:05 PM, Sam Owre <owre@xxxxxxxxxxx> wrote:
> >>>> 
> >>>> Hi Ben,
> >>>> 
> >>>> We tried to capture dimensions and units using the PVS type system, and
> >>>> failed.  Since then we have started adding it to PVS, then worked on
> >>>> adding it to Simulink, and wrote a paper laying out the theory:
> >>>> 
> >>>> Automatic Dimensional Analysis of Cyber-Physical Systems,
> >>>> by Sam Owre, Indranil Saha, and Natarajan Shankar,
> >>>> in FM 2012: Formal Methods Lecture Notes in Computer Science pages 356-371.
> >>>> 
> >>>> We will continue adding it to PVS when there is time available.
> >>>> 
> >>>> As for your proof, you should try 'C-u M-x show-expanded-sequent'; this
> >>>> often shows where mismatches occur.  My guess is you have two different
> >>>> '+' operators.
> >>>> 
> >>>> If you still have problems, please send your specs to me so I can debug
> >>>> this.
> >>>> 
> >>>> Thanks,
> >>>> Sam
> >>>> 
> >>>> 
> >>>> Ben Hocking <ben.hocking@xxxxxxxxxxxxxxxxxxxxxxx> wrote:
> >>>> 
> >>>>> For lengths, I’ve tried creating a “lengths” theory similar to the reals theory in the PVS
> >>>>> prelude, but I’m stuck here:
> >>>>> length_plus_length_is_length :
> >>>>> 
> >>>>> |-------
> >>>>> {1}   FORALL (x, y): length_pred(x + y)
> >>>>> 
> >>>>> Rule? (skeep)
> >>>>> Skolemizing and keeping names of the universal formula in (+ -),
> >>>>> this simplifies to:
> >>>>> length_plus_length_is_length :
> >>>>> 
> >>>>> |-------
> >>>>> {1}   length_pred(x + y)
> >>>>> 
> >>>>> Rule? (lemma "lengths.closed_plus" ("x" "x" "y" "y"))
> >>>>> Applying lengths.closed_plus where
> >>>>> x gets x,
> >>>>> y gets y,
> >>>>> this simplifies to:
> >>>>> length_plus_length_is_length :
> >>>>> 
> >>>>> {-1}  length_pred(x + y)
> >>>>> |-------
> >>>>> [1]   length_pred(x + y)
> >>>>> 
> >>>>> Rule?
> >>>>> 
> >>>>> I’ve tried “assert”, “smash”, “grind”, etc., but nothing seems to resolve this seemingly
> >>>>> simple statement…
> >>>>> 
> >>>>> (Note that length_pred is an undefined function that I’ve attempted to “define” via axioms,
> >>>>> such as closed_plus, etc.)
> >>>>> 
> >>>>> Best Regards,
> >>>>> Ben Hocking
> >>>>> ben.hocking@xxxxxxxxxxxxxxxxxxxxxxx
> >>>>> 
> >>>>>  On Apr 22, 2015, at 9:15 AM, Ben Hocking <ben.hocking@xxxxxxxxxxxxxxxxxxxxxxx> wrote:
> >>>>> 
> >>>>>  Alas, it appears that the simplicity comes with a price. I cannot figure out a way to
> >>>>>  prevent meters and seconds from being added together, or more importantly of determining
> >>>>>  whether a particular measurement is of time, length, or is unitless (as examples).
> >>>>> 
> >>>>>  Best Regards,
> >>>>>  Ben Hocking
> >>>>>  ben.hocking@xxxxxxxxxxxxxxxxxxxxxxx
> >>>>> 
> >>>>>      On Apr 22, 2015, at 8:01 AM, Ben Hocking <ben.hocking@xxxxxxxxxxxxxxxxxxxxxxx>
> >>>>>      wrote:
> >>>>> 
> >>>>>      Viorel,
> >>>>> 
> >>>>>      I really like the idea of using uninterpreted positive real constants. This is far
> >>>>>      simpler than the approach I’ve been using.
> >>>>> 
> >>>>>      Best Regards,
> >>>>>      Ben Hocking
> >>>>>      ben.hocking@xxxxxxxxxxxxxxxxxxxxxxx
> >>>>> 
> >>>>>          On Apr 22, 2015, at 4:51 AM, Viorel Preoteasa <viorel.preoteasa@xxxxxxxx> wrote:
> >>>>> 
> >>>>>          You can also do something like:
> >>>>> 
> >>>>>            m: posreal
> >>>>>            cm: posreal = m / 100
> >>>>>            m_to_cm: lemma 2.5 * m = 250 * cm
> >>>>> 
> >>>>>          Best regards,
> >>>>> 
> >>>>>          Viorel Preoteasa
> >>>>> 
> >>>>>          On 04/22/2015 01:16 AM, Ben Hocking wrote:
> >>>>> 
> >>>>>              Is anyone familiar with work that has been done on unit composition in
> >>>>>              formal specifications within PVS? E.g., verifying that when you multiply
> >>>>>              meters by meters you get square meters?
> >>>>> 
> >>>>>              I have some ideas on what I want to do (and have actually started down that
> >>>>>              path), but I don’t want to reinvent the wheel if this has already been done.
> >>>>> 
> >>>>>              Best Regards,
> >>>>>              Ben Hocking
> >>>>>              ben.hocking@xxxxxxxxxxxxxxxxxxxxxxx
> >>>>> 
> >> 
> > 
>