From eff48a1c6e993a9d2bfa2b07453a90504a32820b Mon Sep 17 00:00:00 2001 From: ProgramSnail Date: Sun, 17 May 2026 17:09:14 +0000 Subject: [PATCH] struct: minor model fixes, read combination fix --- model_with_structures/model.typ | 19 ++++++--- model_with_structures/synthesizer.ml | 3 +- model_with_structures/tests.ml | 2 +- model_with_structures/tests_f.ml | 64 +++++++++++----------------- 4 files changed, 39 insertions(+), 49 deletions(-) diff --git a/model_with_structures/model.typ b/model_with_structures/model.typ index 937a1f5..1912a7b 100644 --- a/model_with_structures/model.typ +++ b/model_with_structures/model.typ @@ -286,18 +286,25 @@ $X$ - можество переменных #let types = $Gamma$ #let envv = $#[env]_Sigma$ #let envt = $#[env]_Gamma$ -$sigma : envv := X -> LL, space vals : envv$ - #[ метки памяти перменных контекста, частично определённая функция ] -$sigma : envt := X -> type, space types : envt$ - #[ типы значений перменных контекста, частично определённая функция ] +$envv := X -> LL, space vals : envv$ - #[ метки памяти перменных контекста, частично определённая функция ] +$envt := X -> type, space types : envt$ - #[ типы значений перменных контекста, частично определённая функция ] $revpath$ - путь в обратную сторону, используется для обновления значений $action$ - действия, совершаемые с примитивным значением, модифицирующие содержащуюся таминформацию -// $DD : X -> decl$ - глобальные определения, частично определённая функция - -// $d in decl, $ -$s in stmt, f in X, x in X, a in X, p in path, pi in revpath$ +- $r in readTag, w in writeTag$ +- $c in copyTag$ +- $i in inTag, o in outTag$ +- $s in stmt$ +- $f, x, a in X$ +- $a in action$ +- $p in path$ +- $v in value$ +- $v_m in vmem, v_r in vread, v_w in vwrite$ +- $t, u in type$ +- $pi in revpath$ === Path Accessors diff --git a/model_with_structures/synthesizer.ml b/model_with_structures/synthesizer.ml index 19a93e2..a60eafd 100644 --- a/model_with_structures/synthesizer.ml +++ b/model_with_structures/synthesizer.ml @@ -757,8 +757,7 @@ struct { u == ZeroRV & v == ZeroRV & u' == ZeroRV } | { u == TopRV & v == ZeroRV & u' == ZeroRV } | { u == ZeroRV & v == TopRV & u' == ZeroRV } | - { u =/= TopRV & v =/= TopRV & - u =/= ZeroRV & v =/= ZeroRV & + { { u == OneRV | { u =/= OneRV & v == OneRV } } & u' == OneRV } } diff --git a/model_with_structures/tests.ml b/model_with_structures/tests.ml index 2325fee..5433e74 100644 --- a/model_with_structures/tests.ml +++ b/model_with_structures/tests.ml @@ -89,7 +89,7 @@ let%expect_test "presentation test 1 (simple types), synt" = print_endline(prog_ [%expect {| [[Cp; Cp; Cp; Cp; Cp; Cp]; [Cp; Cp; Cp; Cp; Cp; Rf]; [Cp; Cp; Cp; Rf; Cp; Cp]; [Cp; Cp; Cp; Rf; Cp; Rf]; [Cp; Rf; Cp; Cp; Cp; Cp]; [Cp; Rf; Cp; Cp; Cp; Rf]; [Cp; Rf; Cp; Rf; Cp; Cp]; [Cp; Rf; Cp; Rf; Cp; Rf]; [Rf; Cp; Cp; Cp; Cp; Cp]; [Rf; Rf; Cp; Cp; Cp; Cp]; [Rf; Cp; Cp; Cp; Cp; Rf]; [Rf; Rf; Cp; Cp; Cp; Rf]; [Rf; Cp; Cp; Rf; Cp; Cp]; [Rf; Rf; Cp; Rf; Cp; Cp]; [Rf; Cp; Cp; Rf; Cp; Rf]; [Rf; Rf; Cp; Rf; Cp; Rf]] |}] let%expect_test "presentation test 2 (complex types), eval" = print_endline(prog_eval_t_presentation_complex_tp ()); - [%expect {| [StEnv (MemEnv ([FunV ([SeqS (SeqS (ReadS (AccessP (DerefP (AccessP (VarP (O), S (O))), O)), SeqS (ReadS (AccessP (DerefP (AccessP (VarP (O), S (O))), S (O))), SeqS (WriteS (AccessP (DerefP (AccessP (VarP (O), S (O))), O)), SeqS (WriteS (AccessP (DerefP (AccessP (VarP (O), S (O))), S (O))), SeqS (ReadS (AccessP (DerefP (AccessP (VarP (O), O)), S (O))), SeqS (WriteS (AccessP (DerefP (AccessP (VarP (O), O)), S (O))), SkipS)))))), SeqS (WriteS (DerefP (AccessP (VarP (O), S (S (O))))), SeqS (ReadS (AccessP (DerefP (AccessP (VarP (O), S (O))), O)), SeqS (ReadS (AccessP (DerefP (AccessP (VarP (O), S (O))), S (O))), SeqS (ReadS (DerefP (AccessP (VarP (O), S (S (O))))), SeqS (ReadS (AccessP (DerefP (AccessP (VarP (O), O)), O)), SeqS (ReadS (AccessP (DerefP (AccessP (VarP (O), O)), S (O))), SeqS (ReadS (AccessP (DerefP (AccessP (VarP (O), O)), S (S (O)))), SkipS))))))))]); TupleV ([RefV (S (S (S (S (S (O)))))); RefV (S (S (S (S (O))))); RefV (S (S (S (O))))]); TupleV ([UnitV (ZeroMV, OneRV, ZeroWV); UnitV (ZeroMV, OneRV, ZeroWV); UnitV (ZeroMV, OneRV, ZeroWV)]); TupleV ([UnitV (ZeroMV, OneRV, ZeroWV); UnitV (ZeroMV, OneRV, ZeroWV)]); UnitV (ZeroMV, TopRV, OneWV); UnitV (ZeroMV, ZeroRV, ZeroWV); TupleV ([UnitV (ZeroMV, ZeroRV, ZeroWV); UnitV (ZeroMV, ZeroRV, ZeroWV)]); TupleV ([UnitV (ZeroMV, ZeroRV, ZeroWV); UnitV (ZeroMV, ZeroRV, ZeroWV); UnitV (ZeroMV, ZeroRV, ZeroWV)])], S (S (S (S (S (S (S (S (O))))))))), TypesEnv ([(S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))), FunT ([(Mode (In, NOut), TupleT ([RefT (Cp, TupleT ([UnitT (Rd, NeverWr); UnitT (Rd, AlwaysWr); UnitT (Rd, NeverWr)])); RefT (Cp, TupleT ([UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr)])); RefT (Cp, UnitT (NRd, AlwaysWr))]))])); (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))), TupleT ([RefT (Cp, TupleT ([UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr)])); RefT (Cp, TupleT ([UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr)])); RefT (Cp, UnitT (Rd, AlwaysWr))])); (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), UnitT (Rd, AlwaysWr)); (S (S (S (S (S (S (S (S (S (S (S (O))))))))))), TupleT ([UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr)])); (S (S (S (S (S (S (S (S (S (S (O)))))))))), TupleT ([UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr)]))], [(S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))), FunT ([(Mode (In, NOut), TupleT ([RefT (Cp, TupleT ([UnitT (Rd, NeverWr); UnitT (Rd, AlwaysWr); UnitT (Rd, NeverWr)])); RefT (Cp, TupleT ([UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr)])); RefT (Cp, UnitT (NRd, AlwaysWr))]))])); (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))), TupleT ([RefT (Cp, TupleT ([UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr)])); RefT (Cp, TupleT ([UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr)])); RefT (Cp, UnitT (Rd, AlwaysWr))])); (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), UnitT (Rd, AlwaysWr)); (S (S (S (S (S (S (S (S (S (S (S (O))))))))))), TupleT ([UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr)])); (S (S (S (S (S (S (S (S (S (S (O)))))))))), TupleT ([UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr)]))]), ValsEnv ([(S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))), S (S (S (S (S (S (S (O)))))))); (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))), S (S (S (S (S (S (O))))))); (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), S (S (O))); (S (S (S (S (S (S (S (S (S (S (S (O))))))))))), S (O)); (S (S (S (S (S (S (S (S (S (S (O)))))))))), O)], [(S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))), S (S (S (S (S (S (S (O)))))))); (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))), S (S (S (S (S (S (O))))))); (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), S (S (O))); (S (S (S (S (S (S (S (S (S (S (S (O))))))))))), S (O)); (S (S (S (S (S (S (S (S (S (S (O)))))))))), O)]), VisitedEnv ([SeqS (SeqS (ReadS (AccessP (DerefP (AccessP (VarP (O), S (O))), O)), SeqS (ReadS (AccessP (DerefP (AccessP (VarP (O), S (O))), S (O))), SeqS (WriteS (AccessP (DerefP (AccessP (VarP (O), S (O))), O)), SeqS (WriteS (AccessP (DerefP (AccessP (VarP (O), S (O))), S (O))), SeqS (ReadS (AccessP (DerefP (AccessP (VarP (O), O)), S (O))), SeqS (WriteS (AccessP (DerefP (AccessP (VarP (O), O)), S (O))), SkipS)))))), SeqS (WriteS (DerefP (AccessP (VarP (O), S (S (O))))), SeqS (ReadS (AccessP (DerefP (AccessP (VarP (O), S (O))), O)), SeqS (ReadS (AccessP (DerefP (AccessP (VarP (O), S (O))), S (O))), SeqS (ReadS (DerefP (AccessP (VarP (O), S (S (O))))), SeqS (ReadS (AccessP (DerefP (AccessP (VarP (O), O)), O)), SeqS (ReadS (AccessP (DerefP (AccessP (VarP (O), O)), S (O))), SeqS (ReadS (AccessP (DerefP (AccessP (VarP (O), O)), S (S (O)))), SkipS))))))))]))] |}] + [%expect {| [StEnv (MemEnv ([FunV ([SeqS (ChoiceS (SeqS (ReadS (DerefP (AccessP (VarP (O), S (O)))), SeqS (WriteS (DerefP (AccessP (VarP (O), S (O)))), SeqS (ReadS (AccessP (DerefP (AccessP (VarP (O), O)), S (O))), SeqS (WriteS (AccessP (DerefP (AccessP (VarP (O), O)), S (O))), SkipS)))), SkipS), SeqS (WriteS (DerefP (AccessP (VarP (O), S (S (O))))), SeqS (ReadS (VarP (O)), SkipS))); SeqS (ChoiceS (SeqS (ReadS (DerefP (AccessP (VarP (O), S (O)))), SeqS (WriteS (DerefP (AccessP (VarP (O), S (O)))), SeqS (ReadS (AccessP (DerefP (AccessP (VarP (O), O)), S (O))), SeqS (WriteS (AccessP (DerefP (AccessP (VarP (O), O)), S (O))), SkipS)))), SkipS), SeqS (WriteS (DerefP (AccessP (VarP (O), S (S (O))))), SeqS (ReadS (VarP (O)), SkipS)))]); TupleV ([RefV (S (S (S (S (S (O)))))); RefV (S (S (S (S (O))))); RefV (S (S (S (O))))]); TupleV ([UnitV (ZeroMV, OneRV, ZeroWV); UnitV (ZeroMV, OneRV, ZeroWV); UnitV (ZeroMV, OneRV, ZeroWV)]); TupleV ([UnitV (ZeroMV, OneRV, ZeroWV); UnitV (ZeroMV, OneRV, ZeroWV)]); UnitV (ZeroMV, TopRV, OneWV); UnitV (ZeroMV, ZeroRV, ZeroWV); TupleV ([UnitV (ZeroMV, ZeroRV, ZeroWV); UnitV (ZeroMV, ZeroRV, ZeroWV)]); TupleV ([UnitV (ZeroMV, ZeroRV, ZeroWV); UnitV (ZeroMV, ZeroRV, ZeroWV); UnitV (ZeroMV, ZeroRV, ZeroWV)])], S (S (S (S (S (S (S (S (O))))))))), TypesEnv ([(S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))), FunT ([(Mode (In, NOut), TupleT ([RefT (Cp, TupleT ([UnitT (Rd, NeverWr); UnitT (Rd, MayWr); UnitT (Rd, NeverWr)])); RefT (Cp, TupleT ([UnitT (Rd, MayWr); UnitT (Rd, MayWr)])); RefT (Cp, UnitT (NRd, AlwaysWr))]))])); (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))), TupleT ([RefT (Cp, TupleT ([UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr)])); RefT (Cp, TupleT ([UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr)])); RefT (Cp, UnitT (Rd, AlwaysWr))])); (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), UnitT (Rd, AlwaysWr)); (S (S (S (S (S (S (S (S (S (S (S (O))))))))))), TupleT ([UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr)])); (S (S (S (S (S (S (S (S (S (S (O)))))))))), TupleT ([UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr)]))], [(S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))), FunT ([(Mode (In, NOut), TupleT ([RefT (Cp, TupleT ([UnitT (Rd, NeverWr); UnitT (Rd, MayWr); UnitT (Rd, NeverWr)])); RefT (Cp, TupleT ([UnitT (Rd, MayWr); UnitT (Rd, MayWr)])); RefT (Cp, UnitT (NRd, AlwaysWr))]))])); (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))), TupleT ([RefT (Cp, TupleT ([UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr)])); RefT (Cp, TupleT ([UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr)])); RefT (Cp, UnitT (Rd, AlwaysWr))])); (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), UnitT (Rd, AlwaysWr)); (S (S (S (S (S (S (S (S (S (S (S (O))))))))))), TupleT ([UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr)])); (S (S (S (S (S (S (S (S (S (S (O)))))))))), TupleT ([UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr)]))]), ValsEnv ([(S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))), S (S (S (S (S (S (S (O)))))))); (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))), S (S (S (S (S (S (O))))))); (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), S (S (O))); (S (S (S (S (S (S (S (S (S (S (S (O))))))))))), S (O)); (S (S (S (S (S (S (S (S (S (S (O)))))))))), O)], [(S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))), S (S (S (S (S (S (S (O)))))))); (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))), S (S (S (S (S (S (O))))))); (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), S (S (O))); (S (S (S (S (S (S (S (S (S (S (S (O))))))))))), S (O)); (S (S (S (S (S (S (S (S (S (S (O)))))))))), O)]), VisitedEnv ([SeqS (ChoiceS (SeqS (ReadS (DerefP (AccessP (VarP (O), S (O)))), SeqS (WriteS (DerefP (AccessP (VarP (O), S (O)))), SeqS (ReadS (AccessP (DerefP (AccessP (VarP (O), O)), S (O))), SeqS (WriteS (AccessP (DerefP (AccessP (VarP (O), O)), S (O))), SkipS)))), SkipS), SeqS (WriteS (DerefP (AccessP (VarP (O), S (S (O))))), SeqS (ReadS (VarP (O)), SkipS))); SeqS (ChoiceS (SeqS (ReadS (DerefP (AccessP (VarP (O), S (O)))), SeqS (WriteS (DerefP (AccessP (VarP (O), S (O)))), SeqS (ReadS (AccessP (DerefP (AccessP (VarP (O), O)), S (O))), SeqS (WriteS (AccessP (DerefP (AccessP (VarP (O), O)), S (O))), SkipS)))), SkipS), SeqS (WriteS (DerefP (AccessP (VarP (O), S (S (O))))), SeqS (ReadS (VarP (O)), SkipS))); SeqS (ChoiceS (SeqS (ReadS (DerefP (AccessP (VarP (O), S (O)))), SeqS (WriteS (DerefP (AccessP (VarP (O), S (O)))), SeqS (ReadS (AccessP (DerefP (AccessP (VarP (O), O)), S (O))), SeqS (WriteS (AccessP (DerefP (AccessP (VarP (O), O)), S (O))), SkipS)))), SkipS), SeqS (WriteS (DerefP (AccessP (VarP (O), S (S (O))))), SeqS (ReadS (VarP (O)), SkipS))); SeqS (ChoiceS (SeqS (ReadS (DerefP (AccessP (VarP (O), S (O)))), SeqS (WriteS (DerefP (AccessP (VarP (O), S (O)))), SeqS (ReadS (AccessP (DerefP (AccessP (VarP (O), O)), S (O))), SeqS (WriteS (AccessP (DerefP (AccessP (VarP (O), O)), S (O))), SkipS)))), SkipS), SeqS (WriteS (DerefP (AccessP (VarP (O), S (S (O))))), SeqS (ReadS (VarP (O)), SkipS)))]))] |}] let%expect_test "presentation test 2 (complex types), synt" = print_endline(prog_synt_t_presentation_complex_tp ()); [%expect {| [[Cp; Cp; Cp]; [Cp; Cp; Rf]; [Cp; Rf; Cp]; [Cp; Rf; Rf]] |}] diff --git a/model_with_structures/tests_f.ml b/model_with_structures/tests_f.ml index 8022138..dccaa23 100644 --- a/model_with_structures/tests_f.ml +++ b/model_with_structures/tests_f.ml @@ -792,32 +792,27 @@ let prog_eval_t_presentation_complex_tp _ = show(answer) (Stream.take (run q timeE == UnitE & requestE == TupleE [RefE userVID; RefE dataVID; RefE timeVID] & - fresh data_p0, data_p1, time_p, - user_id_p, user_name_p, user_surname_p in - access_deref_accesso 0 1 0 data_p0 & - access_deref_accesso 1 1 0 data_p1 & + fresh data_p, time_p, + user_id_p, user_name_p in + deref_accesso 1 0 data_p & deref_accesso 2 0 time_p & access_deref_accesso 0 0 0 user_id_p & access_deref_accesso 1 0 0 user_name_p & - access_deref_accesso 2 0 0 user_surname_p & - seqo [ReadS data_p0; - ReadS data_p1; - WriteS data_p0; - WriteS data_p1; - + seqo [ReadS data_p; + WriteS data_p; ReadS user_name_p; WriteS user_name_p] sendBranchStmts & - seqo [sendBranchStmts; (* TMP *) - (* TODO: FIXME *) - (* ChoiceS (sendBranchStmts, SkipS); *) + seqo [ChoiceS (sendBranchStmts, SkipS); WriteS time_p; - ReadS data_p0; - ReadS data_p1; - ReadS time_p; - ReadS user_id_p; - ReadS user_name_p; - ReadS user_surname_p] sendStmts & + ReadS (VarP 0) + (* ReadS data_p0; *) + (* ReadS data_p1; *) + (* ReadS time_p; *) + (* ReadS user_id_p; *) + (* ReadS user_name_p; *) + (* ReadS user_surname_p *) + ] sendStmts & (* sendStmts == SkipS & *) sendD == FunD ([(Mode (In, NOut), requestArgsT)], sendStmts) & @@ -828,11 +823,8 @@ let prog_eval_t_presentation_complex_tp _ = show(answer) (Stream.take (run q seqo [ CallS (VarP sendFID, [PathE (VarP requestVID)]); WriteS time_gp; - (* TODO: FIXME *) - (* ChoiceS (ReadS user_name_gp, *) - (* ReadS user_surname_gp); *) - ReadS user_name_gp; (* TMP *) - ReadS user_surname_gp; (* TMP *) + ChoiceS (ReadS user_name_gp, + ReadS user_surname_gp); ReadS time_gp ] stmts & prog == Prg ([ @@ -884,12 +876,9 @@ let prog_synt_t_presentation_complex_tp _ = show(answerCpCapList) (Stream.take ( access_deref_accesso 2 0 0 user_surname_p & seqo [ReadS data_p; WriteS data_p; - ReadS user_name_p; WriteS user_name_p] sendBranchStmts & - seqo [sendBranchStmts; (* TMP *) - (* TODO: FIXME *) - (* ChoiceS (sendBranchStmts, SkipS); *) + seqo [ChoiceS (sendBranchStmts, SkipS); WriteS time_p; ReadS (VarP 0) ] sendStmts & @@ -903,10 +892,8 @@ let prog_synt_t_presentation_complex_tp _ = show(answerCpCapList) (Stream.take ( seqo [ CallS (VarP sendFID, [PathE (VarP requestVID)]); WriteS time_gp; - (* TODO: FIXME *) - (* ChoiceS (ReadS user_name_gp, *) - (* ReadS user_surname_gp); *) - ReadS user_name_gp; (* TMP *) + ChoiceS (ReadS user_name_gp, + ReadS user_surname_gp); ReadS user_surname_gp; (* TMP *) ReadS time_gp ] stmts & @@ -1031,9 +1018,8 @@ let prog_eval_compl_test_send _ = show(answer) (Stream.take (run q ReadS sb_access3] sendFBranch & seqo [ChoiceS (sendFBranch, SkipS); - WriteS (AccessP (VarP 0, 4)); - (* TODO: read all the substructure ?? *) - ReadS (AccessP (VarP 0, 4)) (*rdS v0*)] (* FIXME: TMP, parial read, should be full *) + WriteS (VarP 0)); + ReadS (VarP 0))] sendF & fresh sa_access0, sa_access1, sa_access2, sa_access3 in @@ -1041,7 +1027,7 @@ let prog_eval_compl_test_send _ = show(answer) (Stream.take (run q access_deref_accesso 1 1 0 sa_access1 & access_deref_access_deref_accesso 0 0 0 0 sa_access2 & access_deref_accesso 0 1 0 sa_access3 & - seqo [WriteS (AccessP (VarP 0, 4)) (*wrS v0*); (* FIXME: TMP, parial write, should be full *) + seqo [WriteS (VarP 0)); CallS (VarP sendID, [PathE (VarP 0)]); CallS (VarP get_version_idID, [PathE (VarP 0)]); CallS (VarP updated_versionID, [PathE (VarP 0)]); @@ -1317,8 +1303,7 @@ let prog_synt_compl_test_send _ = show(answerCpCapList) (Stream.take (run q sendFBranch & seqo [ChoiceS (sendFBranch, SkipS); WriteS (AccessP (VarP 0, 4)); - (* TODO: read all the substructure ?? *) - ReadS (AccessP (VarP 0, 4)) (*rdS v0*)] (* FIXME: TMP, parial read, should be full *) + ReadS (VarP 0)] sendF & fresh sa_access0, sa_access1, sa_access2, sa_access3 in @@ -1326,11 +1311,10 @@ let prog_synt_compl_test_send _ = show(answerCpCapList) (Stream.take (run q access_deref_accesso 1 1 0 sa_access1 & access_deref_access_deref_accesso 0 0 0 0 sa_access2 & access_deref_accesso 0 1 0 sa_access3 & - seqo [WriteS (AccessP (VarP 0, 4)) (*wrS v0*); (* FIXME: TMP, parial write, should be full *) + seqo [WriteS (AccessP (VarP 0, 4)); CallS (VarP sendID, [PathE (VarP 0)]); CallS (VarP get_version_idID, [PathE (VarP 0)]); CallS (VarP updated_versionID, [PathE (VarP 0)]); - (* TODO: read all the substructure ?? *) WriteS sa_access0; WriteS sa_access1; ChoiceS (