LabelLabel

ioa_mentions_trace(A)

([[A.da]] rho) List

[[I]] rho A.ds < > de e x mk_trace_env(tr, te)

(t:dec(). t A.da & t.lbl = kind(act)) [[I]] rho A.ds < > de e x' tappend(mk_trace_env(tr, te);act)

[[wp(A;kind(act);I)]] rho A.ds dec_lookup(A.da;kind(act)) de e x value(act) tappend(mk_trace_env(tr, te);act) [[I]] rho A.ds < > de e x' tappend(mk_trace_env(tr, te);act)

[[I]] rho A.ds < > de e x' tappend(mk_trace_env(tr, te);act)

1

2. I: Collection(rel()) 3. rho: Decl 4. de: sig() 5. e: {[[de]] rho} 6. te: LabelLabel 7. tc_ioa(A;de) 8. ioa_mentions_trace(A) 9. trace_consistent_pred(rho;A.da;te;I) 10. tc_pred(I;A.ds; < > ;de) 11. covers_pred(A;I) 12. guarded_trace(A.da;te;I) 13. closed_pred(I) 14. single_valued_decls(A.ds) 15. s0: [[A]] rho de e.state 16. x: [[A]] rho de e.state 17. act: [[A]] rho de e.action 18. x': [[A]] rho de e.state 19. tr: ([[A.da]] rho) List 20. [[A]] rho de e.init(s0) 21. trace_reachable([[A]] rho de e;s0;mk_trace_env(tr, te).trace;x) 22. r:rel(). r I [[r]] rho A.ds < > de e x mk_trace_env(tr, te) 23. [[A]] rho de e.trans(x,act,x') 24. (t:dec(). t A.da & t.lbl = kind(act)) (r:rel(). r I [[r]] rho A.ds < > de e x' tappend(mk_trace_env(tr, te);act)) 25. (r:rel(). r wp(A;kind(act);I) [[r]] rho A.ds dec_lookup(A.da;kind(act)) de e x value(act) tappend(mk_trace_env(tr, te);act)) (r:rel(). r I [[r]] rho A.ds < > de e x' tappend(mk_trace_env(tr, te);act)) 26. r: rel() 27. r I [[r]] rho A.ds < > de e x' tappend(mk_trace_env(tr, te);act)

About: