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

PROGRAM-ERROR using inst?



I'm getting an odd PROGRAM-ERROR from pvs when I use (inst?).  Could
someone tell me if I am doing something odd that would cause this.  I
have included the dump file of the theory and the proof that I am
working on.  If you rerun the proof of 'test_setTime' then try to
instantiate using (inst?) I get the following error:

{-1}    (FORALL (pkt: TimePkt, nodeID: NodeID, net: Network):
         executePacket(pkt, nodeID, net)
             = IF secure(setTimePkt(pkt, nodeID, net)) THEN
setTimePkt(pkt, nodeID, net) ELSE net ENDIF)
  |-------
[1]    (curTime(node(executePacket((# src := node1, dest := node3,
time := 1 #), node3,
                                  (# node :=
                                       (LAMBDA (n: NodeID):
                                          nullNode
                                            WITH [(id) := node1,
                                                  (route)(node3)
                                                  := node2])
                                         WITH [(node1) :=
                                                 nullNode
                                                   WITH [(id)
                                                         := node1,
                                                         (route)(node3)
                                                         := node2],
                                               (node2) :=
                                                 nullNode
                                                   WITH [(id)
                                                         := node2,
                                                         (route)(node3)
                                                         := node3],
                                               (node3) :=
                                                 nullNode
                                                   WITH [(id)
                                                         := node2,
                                                         (route)(node3)
                                                         := node3]]
                                     #)
                                    WITH [(node)(node1)(curTime) |->
1,
                                          (node)(node2)(curTime)
                                          |-> 1]))(node2))
           = 1)

Rule? (inst? -1 :WHERE 1)
Found substitution:
net gets (# node :=
     (LAMBDA (n: NodeID): nullNode WITH [(id) := node1, (route)(node3)
:= node2])
       WITH [(node1) := nullNode WITH [(id) := node1, (route)(node3)
:= node2],
             (node2) := nullNode WITH [(id) := node2, (route)(node3)
:= node3],
             (node3) := nullNode WITH [(id) := node2, (route)(node3)
:= node3]]
   #)
  WITH [(node)(node1)(curTime) |-> 1, (node)(node2)(curTime) |-> 1],
nodeID gets node3,
pkt gets (# src := node1, dest := node3, time := 1 #),
Error: No methods applicable for generic function
#<STANDARD-GENERIC-FUNCTION ID> with args (NIL) of classes (NULL)
  [condition type: PROGRAM-ERROR]

Restart actions (select using :continue):
 0: Try calling it again

% Begin dump file
%Patch files loaded: patch2 version 2.417

$$$pvs-strategies
(defstep expand-governservice ()
  (repeat (try (expand "governService" :OCCURRENCE 1)
     (try (lift-if)
       (try (expand "svcCanBeGoverned") 
         (skip) 
         (skip))
       (skip))
     (skip)))
;;(lift-if)(expand "svcCanBeGoverned"))
  "Strategy used to eliminate governService from terms"
  "Expanding governService, if-lifting, expanding svcCanBeGoverned")


(defstep expand-certificate ()
  (then@ (expand "getResource")
    (expand "getBootLevelResource")
    (expand "installAEGISResources")
    (expand "installResource")
    (expand "setResource"))
  "Strategy used to prove a certificate resource is valid"
  "Expanding resources")

(defstep expand-installservice (&optional fnum)
  (try (expand "installService" fnum :occurrence 1)
    (try (expand "installService" fnum :occurrence 1)
      (try (expand "governService" fnum :occurrence 1)
        (try (lift-if)
          (try (split)
            (try (flatten)
                 (skip))
               (skip))
             (skip))
           (skip))
         (skip))
       (skip))
     (skip))
   (skip))
  "Strategy used to eliminate installService from terms"
  "Expanding governService, if-lifting, expanding svcCanBeGoverned")



$$$Resources.pvs
Resources  % [ parameters ]
		: THEORY

  BEGIN

  % ASSUMING
   % assuming declarations
  % ENDASSUMING

% Lets say I have two resources 
% 
%   curTime - The current time of the active node
%   curTemp - The current tempreature at the node
% 

Resource : TYPE = {
  curTime,
  curTemp,
  route
}

Address : TYPE
Packet : TYPE = [#
  src : Address,
  dest : Address
#]

NodeID : TYPE = {
  nullID,
  node1,
  node2,
  node3
}

Node : TYPE = [#
  id : NodeID,
  resources : set[Resource],
  curTime : integer,
  curTemp : integer,
  route : [NodeID->NodeID]
#]


Network : TYPE = [#
  node : [NodeID -> Node]
#]

secure(net : Network) : boolean = true

% I also have two services
% 
%   getTime - Get the current time of the node
%   setTime - Set the current time of the node
%   getTemp - Get the current temperature at the node
% 
% 
getTime(nodeID : NodeID, net : Network) : integer = 
  LET n = node(net)(nodeID) IN
    curTime(n)

setTime(time : integer, nodeID : NodeID, net : Network) : Network = 
  net WITH [
    (node)(nodeID)(curTime) |-> time
  ]

getTemp(nodeID : NodeID, net : Network) : integer = 
  LET n = node(net)(nodeID) IN
    curTemp(n)

getRoute(src : NodeID, dest : NodeID, net : Network) : NodeID =
  LET n = node(net)(src) IN
    route(n)(dest)

setRoute(nodeID : NodeID, dest: NodeID, next : NodeID, net : Network) : Network =
  LET n = node(net)(nodeID) IN
    net WITH [
      (node)(nodeID) := n WITH [ (route)(dest) := next ]
    ]

% I want to create an active packet that records the time and
% temperature of each active node it encounters on the route it takes to
% its destination.
% 
% 
% I need to specify the execution of the packet.
% 
% 1. Get time on the current node
% 2. Get the temperature on the current node
% 3. Add the time and temperature to the list kept in the packet
% 4. Route this packet to the next node on its journey
% 
TimeTempPkt : TYPE = [#
  src : NodeID,
  dest : NodeID,
  time : sequence[integer],
  temp : sequence[integer]
#]

send(pkt : TimeTempPkt, nodeID : NodeID, net : Network) : Network =
  net

getTimeAndTempPkt(pkt: TimeTempPkt, nodeID : NodeID, net : Network) : Network =
LET 
  newPkt = pkt WITH [
    time := add(getTime(nodeID, net), time(pkt)),
    temp := add(getTemp(nodeID, net), temp(pkt))
  ]
IN
  send(newPkt, nodeID, net)

executePacket(pkt : TimeTempPkt, nodeID : NodeID, net : Network) :
Network = 
  IF dest(pkt) = nodeID THEN
     net
  ELSIF secure(getTimeAndTempPkt(pkt, nodeID, net)) THEN
    getTimeAndTempPkt(pkt, nodeID, net)
  ELSE 
    net
  ENDIF


% 
% Lets say we want to execute a packet that sets the time on each node
% it encounters on its route.
% 
TimePkt : TYPE = [#
  src : NodeID,
  dest : NodeID,
  time : integer
#]

executePacket : [TimePkt, NodeID, Network -> Network]

send(pkt : TimePkt, nodeID : NodeID, net : Network) : Network =
  executePacket(pkt, nodeID, net)

setTimePkt(pkt : TimePkt, nodeID : NodeID, net : Network): Network =
  LET newNet = setTime(time(pkt), nodeID, net) ,
      node = node(newNet)(nodeID) IN
    IF dest(pkt) = nodeID THEN
      newNet
    ELSE
      send(pkt, route(node)(dest(pkt)), newNet)
    ENDIF

%executePacket(pkt : TimePkt, nodeID : NodeID, net : Network) : Network =
executePacket_def : AXIOM
  FORALL (pkt : TimePkt, nodeID : NodeID, net : Network):
    executePacket(pkt, nodeID, net) = 
      IF secure(setTimePkt(pkt, nodeID, net)) THEN
        setTimePkt(pkt, nodeID, net)
      ELSE 
        net
      ENDIF


nullNode : Node = (#
  id := nullID,
  resources := emptyset[Resource],
  curTime := 0,
  curTemp := 0,
  route := (LAMBDA (n:NodeID): n)
#)

test_setTime : THEOREM
  LET 
    n1 = nullNode WITH [ (id) := node1, (route)(node3) := node2 ],
    n2 = nullNode WITH [ (id) := node2, (route)(node3) := node3 ],
    n3 = nullNode WITH [ (id) := node3 ],
    net = (#
      node := (LAMBDA (n: NodeID) : n1)
      WITH [
        (node1) := n1,
        (node2) := n2,
        (node3) := n2
      ]
    #),
    pkt = (#
      src := node1,
      dest := node3,
      time := 1
    #)
  IN
    getTime(node2, send(pkt, node1, net)) = 1


  END Resources

$$$Resources.prf
(|Resources| (|executePacket_def| "" (POSTPONE) NIL)
 (|test_setTime| "" (SIMPLIFY)
  (("" (EXPAND "getTime")
    (("" (EXPAND "send")
      (("" (LEMMA "executePacket_def")
        (("" (INST?)
          (("" (REPLACE -1 1)
            (("" (HIDE -1)
              (("" (LIFT-IF)
                (("" (EXPAND "secure")
                  (("" (EXPAND "setTimePkt")
                    (("" (POSTPONE) NIL))))))))))))))))))))))