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

about the tuple type



Hello,
 
I am demonstrating the stable failure model ( modelled by CSP) using PVS. We use a pair of sets to represent this model, for example, [ set[trace[T]], set[traces[T],set[T]]]], ( here, trace[T]=list[T], T:TYPE, anyway, it doesn't matter). Of course, this is a tuple and the definition is as following:
 
 processes [ T:TYPE ]: THEORY
 
  BEGIN
 
  importing traces
 
 a:VAR T
 t:VAR trace[T]
 X,X1:VAR setof[T]
 
S: VAR [process[T],failure[T]]
 
ok, you could pass these conditions
  %===========================================
  % some conditions for stable failure model
  %===========================================
 
  SF1(S):bool= forall t,X: member((t,X),S`2)=> member(t,S`1) 
  SF2(S):bool= forall t,X,X1: member((t,X),S`2) and  subset?(X1,X)=> member((t,X1),S`2)
  SF3(S):bool= forall a,t,X,X1: member((t,X),S`2) and member(a,X1) and NOT member(append(t,cons(a,null)),S`1)=>member((t,union(X,X1)),S`2)
 
  %===========================================
  %  the definition of stable failure model
  %===========================================
 
  process:TYPE={S| SF1(S) and SF2(S) and SF3(S)}
 
 
  Well, now we got the definition about the process. But how can I do the constant declarations. For example, the odd number ,we define it as 
  odd:[nat->bool] = { n: nat | exists (m:nat): n=2*m+1} 
 
but for this case, it is a tuple but a set. How can I do? for example, as defining the Stop process
 
Stop: process= ........................................ in fact, Stop is a tuple [ {t| t=null}, {(t,X)| t=null and X=fullset}]
 
thank you so much!
 
Kun 
 
 
 
 
  END sf_processes