??? ?????? ? ??????? ??????? ????????? ? ??????????? ??? ??? ??????:
1. ????????? ???????? ?????????? ??????? (invalid end-states). ??????? ?
?????? ???? ?? ??????. ????? ???????????? ?? ???????? ???????? ?????????
? ????????? ???? ? ?????? task5_safety_out.txt.
2. ? ?????? ?? ?????? ???? ????????????? ???? (unreachable code), ??
??????????? ???????? ????????? ????????? (-end-). ???? ????? ??? ?
?????? ??????, ????????? ??.
3. ? ?????? ?? ?????? ???? ?????? ??????????? (non-progress cycles), ??
???????????:
3.1) ?????, ?????????? ? ??????????? ??????????? ???????????? ???????
3.2) ??????, ??????????????? ?????? ???????????? ???????, ???????
????? ?????????? ?????????? ????? ????????????.
????? ???????, ???????????, ??????????? ? ??????
(????????, ??????????????? ??? ????????????? ????????? ??????) ?? ??????
??????? ? ?????? ??????????? ??????.
????? ???????????? ??? ???????? ?????????? ??????
??????????? ????????? ? ????? ? ?????? task5_nonprogress_out.txt. ?????
progress, ??????????????? ??? ????, ????? ??????????? ?? ???????
???????? ?? ??????????? ?????, ????????????? ? ??????? 3.1 ? 3.2, ??????
???? ??????????? ? ?????? model_assert.pml.
4. ????????????? ???? ???????? ??????? ? ??????? ?????? ?????????
??????? ? ??????? Spin, ????????? ? ??????? Spin. ??? ???? ?? ??????
?????????????? ?????-???? ??????????????? ??????????. ????????????
????????? ? ????? ? ??????? spec.ltl:
4.1. ? ???? ?????????? ???? ??????? ???? ??? ?????? ??????????
??????? ??????? ??????? ??? ?????? ?????????? ?????? *alloc*.
4.2. ? ???? ?????????? ???? ??????? ????? ????????? ??????? ???????
???? ??? ?????? ?????? ????????????? ??? ?????? ?????? *free*,
4.3. ?? ?????? ????? ????????? ??????? ????????? ? ????????????
??????? ??????????? ???????? ?????? ?? ????????? ????????.
4.4. ? ??????????? ?????? (????? ???????? spin_lock* ?
spin_unlock*) ????? ?????????? ?? ????? ?????? ????????.
4.5. ? ???? ?????????? ???? ???????, ??????? kfree ?????????? ??
????? ?????? ????.
????????, ??? ???????? ???????? ??????? ?????? ???????? ????????:
????????? ??????, ???????? ??????? ???????????, ???????? ?????????
??????, ?? ???????? ? ??????, ??-??????? ??????? ???????? ??????? ?
??????????? ?????? ???.
5a. ? ??????, ???? ?????? ???????? ????????:
- ???????, ?????? ???????????? ?? ??????????? ?? ???????? ??????;
- ???????, ??? ?????????? ?????? ? ??????;
- ???????, ?????? ????? ?????? ?????????;
- ????????? ???????????, ???????? pan, ? ????? counterexample.txt;
- ????????? ???????? ? ?????????? ?????? ? ?????? task5.pml ?
task5_modified.pml;
- ????????? ????? pan ? ????? task5_ver_out.txt.
5b. ? ??????, ???? ???????????? ?? ??????????? ?? ??????:
- ????????? ???????????, ???????? pan, ? ????? counterexample.txt;
- ????????? ?? ???????????? Spin ??????????? ?? ???????? ?????????;
- ????????? ? ???, ??? ??????????? ?? ???????? ????????? ???????????;
- ????????? ??????????? ?? ???????? ????????? ? ?????
prog_counterexample.txt. ??????????? ?????? ???? ?????? ? ????
?????????????????? ??????? ????? ???????? ????????? ? ???????? ??????????.
- ????????? ?????? ? ????? task5.pml;
- ????????? ????? pan ? ????? task4_ver_out.txt.
- ??????? ??????????????? ???? ?? ????????????? (????????,
«spec_1.ltl») ??? ???????? ?????????? ???????.
5c. ? ??????, ???? ????????? ? ?????? ?? ????????????? ? ????????????
???????????:
- ????????? ?????? ? ????? task4.pml;
- ????????? ????? pan ? ????? ver_out.txt.
??????e ????? ????? -- ?????? 14-18 ???.
?????-?????????-?????-?????-???????? ????? ? ???????? ??????, ??? ??
????? ?????????? ?????? ?? ????????? ???? (?????????? ???? ?????? ?????).
? ?????????,
?????????? ????????.