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

[PVS-Help] Need help with the Choose function



Hello all-
I need help with the choose function. I want to choose the edge from X in my graph and there is only one from (X,Y) however the choose function returns (Y,Z).
 
The below theorem is is trying to prove that an edge can be taken (ie taken=true).
 
However all my code has been simplified down to just just trying to get an outgoing edge from the X vert in the graph. If my choose function picks the only edge in the graph from X then the PC counter would go to LTRUE which gets taken=true.  However right now the choose function always pick (Y,Z).
 
I do not know where I'm going wrong, unless i'm just not using the right commands to prove it.
 
Any help at all would be greatly appreciated.
 
Kelly
 
 
 
 
%Initialize graph
InitGraph: digraph[Entity] = (#vert:= add(X, add(Y, singleton[Entity](Z))), edges:= add((X,Y), add((Y,Z),emptyset[edgetype]))#)
 
I have a node type which is declared:
 
node : TYPE = [#
dest: Entity, % destination
source: Entity, % source edge starts from
e1: edgetype, % an outgoing edge
ie: finite_set[edgetype], % all incoming edges
oe: finite_set[edgetype], % all outgoing edges
oec: nat, %outgoing edge card
iec:nat % incomiing edge card

#]
 
And a node database type declared as a function. as each entity in the graph has node data attached to it.
n_db: TYPE = function[Entity -> node]
 
 
PVS file below. (the files is also attached as ptakerule.pvs, tdd.pvs is the definition theory it imports.)
----------------------------------------------------------------------------------------------------------
pt %[Entity: TYPE+]: THEORY
%SUBJECT ONLY
%Is used strictly for the 3 node query, which is how the rule is defined.
BEGIN

Importing tDefinitions%[Entity]
 
%Initialize graph
InitGraph: digraph[Entity] = (#vert:= add(X, add(Y,
singleton[Entity](Z))), edges:= add((X,Y), add((Y,Z),emptyset[edgetype]))#)
 
%initializes the edge rights
ADD(db: r_db): r_db = db with [(X,Y):= add(take, emptyset[Rights])] with [(Y,Z):= add(read,emptyset[Rights])]
 
%----------------------------------------------------------------------------------------
set_edge(x:Entity,a:edgetype, c:L_Graph,oes: finite_set[edgetype] ): L_Graph = c with [`Node(x)`e1:=a,`Node(x)`oe:=oes ]
 
get_edge(c: L_Graph, x: Entity): L_Graph =
%see if the current edge has take for a right if it does update the dest and source
if empty?(c`Node(x)`oe)
then c
else let a = choose(c`Node(x)`oe) in set_edge(x,a, c, rest(c`Node(x)`oe))
endif
 
XYedge?(c:L_Graph, x:Entity):bool = member((X,Y),c`Node(x)`oe) % this should return true for X
 
YZedge?(c:L_Graph, x:Entity):bool = member((Y,Z),c`Node(x)`oe) % this should return false for X
 
e1?(c:L_Graph, x:Entity):bool= member(c`Node(x)`e1,c`Node(x)`oe)
%----------------------------------------------------------------------------------------
%loop actions
%sets: one
 
L0(c: L_Graph, x:Entity, y:Entity): L_Graph = c with [%g0:= InitGraph,
g1:=InitGraph, db:= ADD(c`db), one:=x ]
 
%sets the node var oe to the outgoing edges and the node variable ie to the incoming edges
get_out_in_edge(x:Entity,oes: finite_set[edgetype], ies: finite_set[edgetype], c:L_Graph): L_Graph = c with [`Node(x)`source:=x,`Node(x)`oe:=oes, `Node(x)`ie:=ies ]
 
TAKE(c: L_Graph, x: Entity, n: n_db):L_Graph = get_edge(c,x)
 
LTRUE(c:L_Graph): L_Graph = c with [taken:= true]
LFALSE(c:L_Graph): L_Graph = c with [taken:= false]
%----------------------------------------------------------------------------------------
%Loop
sw(c: L_Graph, r: Rights, x: Entity, y: Entity): L_Graph =
Cases c`PC of
%initializes graph and r_db
% checks if first node is in graph else quit
L0:L0(c,x,y) with [PC:=L1],
 
%checks if there are at least 3 verts in graph else quit
L1: c with [PC:= if (card[Entity](vert(c`g1))>=3)
then L2
else LFALSE endif],
 
L2: get_out_in_edge(x,outgoing_edges(x, c`g1), incoming_edges(x, c`g1), c) with [PC:= L3], %TAKE
 
L3: c with [PC:=if XYedge?(c, x) then L4 else LFALSE endif], %TAKE
 
L4:c with [PC:=if YZedge?(c, x) then LFALSE else TAKE endif],
 
TAKE: TAKE(c, c`one, c`Node) with [PC:=L5], %TAKE1
 
L5: c with [PC:=if e1?(c, x) then LTRUE else LFALSE endif],
 
LTRUE: LTRUE(c) with [PC:= LEND],
 
LFALSE:LFALSE(c) with [PC:= LEND],
 
LEND: c
Endcases
 
takerule(num: nat, r: Rights, x: Entity, y: Entity, initial: L_Graph ):
Recursive L_Graph =
if num=0 then
initial with [PC:=L0]
else
sw(takerule(num-1,r,x,y,initial),r,x,y)
endif measure num
 
Take_Rule_Taken: theorem
forall (initial: L_Graph):
forall(num: nat | takerule(num, read, X, Z, initial)`PC=LEND):
takerule(num, read, X, Z, initial)`taken=true
 
%(skosimp)(induct "num")(grind)(grind)(induct "j")(grind)(grind)(expand "takerule")(expand "takerule")(grind)(expand "takerule")(expand "takerule")(grind)
%
%(rewrite "card_add")(rewrite "card_add")(rewrite "card_singleton")(grind)
 
END pt


Make distant family not so distant with Windows Vista® + Windows Live™. Start now!
tDefinitions %[Entity: TYPE+]
: THEORY

  BEGIN
Entity: Type = {X,Y,Z}
Importing digraphs@digraphs[Entity]
Importing digraphs@digraph_ops[Entity]
Importing digraphs@digraph_deg[Entity]

	
%declares TYPE of right works
Rights: TYPE = {read, write, take, grant} 

PCT: TYPE = {L0,L00,L3,L31,L20, L01, L001,L0001,L00001, L02,L1,L2,L4,L41,L5,L8,L10,L81,LTRUE,LFALSE,TAKE,TAKE1 ,LEND}

% don't put + on the Types following

r_db: TYPE =function[edgetype[Entity]->set[Rights]]
nil: Entity

node : TYPE = [#
			dest: Entity, % destination
			source: Entity, % source edge starts from
			e1: edgetype, % an outgoing edge
			ie: finite_set[edgetype], % all incoming edges
			oe: finite_set[edgetype], % all outgoing edges
			oec: nat,
			iec:nat
	
			#]

%nodes: TYPE = set[node]
n_db: TYPE = function[Entity -> node]
L_Graph: TYPE = 	[#
		%	g0: digraph[Entity],
			g1: digraph[Entity],
			db: r_db,
			PC: PCT,
			Node: n_db,
			taken: bool,
			one:   Entity,
			two:  Entity,
			three: Entity
			#]

null: edgetype = (nil,nil)
%X,Y,Z: Entity

 END tDefinitions

ptakerule.pvs