Редактирование: Изображение:Pvs tree.png
Материал из eSyr's wiki.
Внимание: Вы не представились системе. Ваш IP-адрес будет записан в историю изменений этой страницы.
Правка может быть отменена. Пожалуйста, просмотрите сравнение версий, чтобы убедиться, что это именно те изменения, которые вас интересуют, и нажмите «Записать страницу», чтобы изменения вступили в силу.
Текущая версия | Ваш текст | ||
Строка 1: | Строка 1: | ||
- | Автор: | + | Автор: Василий Мерзляков. |
Исходный dot-файл: | Исходный dot-файл: | ||
Строка 13: | Строка 13: | ||
"node0" -> "node1" | "node0" -> "node1" | ||
"node2" [ | "node2" [ | ||
- | label = "{ |[1] ( | + | label = "{[-1] i = 0|[1] (i \> 7) IMPLIES EXIST (t : nat, f : nat) : i = 3 * t + 5 * f}" |
shape = "record" | shape = "record" | ||
] | ] | ||
Строка 22: | Строка 22: | ||
"node2" -> "node3" | "node2" -> "node3" | ||
"node4" [ | "node4" [ | ||
- | label = "{[-1] | + | label = "{[-1] i \> 7\n[-2] i = 0|[1] EXIST (t : nat, f : nat) : i = 3 * t + 5 * f}" |
shape = "record" | shape = "record" | ||
] | ] | ||
"node3" -> "node4" | "node3" -> "node4" | ||
+ | "node5" [ | ||
+ | label = "(replace -2)" | ||
+ | ] | ||
+ | "node4" -> "node5" | ||
+ | "node6" [ | ||
+ | label = "{[-1] 0 \> 7\n[-2] i = 0|[1] EXIST (t : nat, f : nat) : i = 3 * t + 5 * f}" | ||
+ | shape = "record" | ||
+ | ] | ||
+ | "node5" -> "node6" | ||
"node7" [ | "node7" [ | ||
label = "(assert)" | label = "(assert)" | ||
Строка 31: | Строка 40: | ||
fillcolor = "green" | fillcolor = "green" | ||
] | ] | ||
- | " | + | "node6" -> "node7" |
"node8" [ | "node8" [ | ||
label = "{ |[1] FORALL (j : nat) :\n(j \> 7) IMPLIES EXIST (t : nat, f : nat) : j = 3 * t + 5 * f\nIMPLIES\n(j + 1 \> 7) IMPLIES EXIST (t : nat, f : nat) : j + 1 = 3 * t + 5 * f}" | label = "{ |[1] FORALL (j : nat) :\n(j \> 7) IMPLIES EXIST (t : nat, f : nat) : j = 3 * t + 5 * f\nIMPLIES\n(j + 1 \> 7) IMPLIES EXIST (t : nat, f : nat) : j + 1 = 3 * t + 5 * f}" | ||
Строка 105: | Строка 114: | ||
"node22" -> "node23" | "node22" -> "node23" | ||
"node24" [ | "node24" [ | ||
- | label = "{[-1] j!1 = 3 * t!1 + 5 * 0\n[-2] j!1 + 1 \> 7|[1] j!1 + 1 = 3 * (t!1 - 3) + 5 * 2}" | + | label = "{[-1] j!1 = 3 * t!1 + 5 * 0\n[-2] f!1 = 0\n[-3] j!1 + 1 \> 7|[1] j!1 + 1 = 3 * (t!1 - 3) + 5 * 2}" |
shape = "record" | shape = "record" | ||
] | ] | ||
Строка 121: | Строка 130: | ||
"node21" -> "node26" | "node21" -> "node26" | ||
"node27" [ | "node27" [ | ||
- | label = "( | + | label = "(assert)" |
+ | style = "filled" | ||
+ | fillcolor = "green" | ||
] | ] | ||
"node26" -> "node27" | "node26" -> "node27" | ||
"node28" [ | "node28" [ | ||
- | label = "{[-1] j!1 = 3 * t!1 + 5 * | + | label = "{[-1] f!1 /= 0\n[-2] j!1 = 3 * t!1 + 5 * f!1\n[-3] j!1 + 1 \> 7|[1] EXIST (t : nat, f : nat) : j!1 + 1 = 3 * t + 5 * f}" |
shape = "record" | shape = "record" | ||
] | ] | ||
- | " | + | "node19" -> "node28" |
"node29" [ | "node29" [ | ||
- | label = "( | + | label = "(inst 1 \"t!1 + 2\" \"f!1 - 1\")" |
- | + | ||
- | + | ||
] | ] | ||
"node28" -> "node29" | "node28" -> "node29" | ||
"node30" [ | "node30" [ | ||
- | label = "{[-1] j!1 = 3 * t!1 + 5 * f!1\n[- | + | label = "{[-1] f!1 /= 0\n[-2] j!1 = 3 * t!1 + 5 * f!1\n[-3] j!1 + 1 \> 7|[1] j!1 + 1 = 3 * (t!1 + 2) + 5 * (f!1 - 1)}" |
shape = "record" | shape = "record" | ||
] | ] | ||
- | " | + | "node29" -> "node30" |
"node31" [ | "node31" [ | ||
- | label = "( | + | label = "(assert)" |
+ | style = "filled" | ||
+ | fillcolor = "green" | ||
] | ] | ||
"node30" -> "node31" | "node30" -> "node31" | ||
"node32" [ | "node32" [ | ||
- | label = "{[-1] j!1 = 3 * t!1 + 5 * f!1\n[- | + | label = "{[-1] f!1 /= 0\n[-2] j!1 = 3 * t!1 + 5 * f!1\n[-3] j!1 + 1 \> 7|[1] f!1 - 1 \>= 0}" |
shape = "record" | shape = "record" | ||
] | ] | ||
- | " | + | "node29" -> "node32" |
"node33" [ | "node33" [ | ||
label = "(assert)" | label = "(assert)" | ||
Строка 156: | Строка 167: | ||
"node32" -> "node33" | "node32" -> "node33" | ||
"node34" [ | "node34" [ | ||
- | label = "{[-1 | + | label = "{[-1] j!1 + 1 \> 7|[1] j!1 \> 7\n[2] EXIST (t : nat, f : nat) : j!1 + 1 = 3 * t + 5 * f}" |
shape = "record" | shape = "record" | ||
] | ] | ||
- | " | + | "node15" -> "node34" [label = "посылку в консеквенты"] |
"node35" [ | "node35" [ | ||
- | label = "( | + | label = "(case \"j!1 = 7\")" |
- | + | ||
- | + | ||
] | ] | ||
"node34" -> "node35" | "node34" -> "node35" | ||
"node36" [ | "node36" [ | ||
- | label = "{[-1] j!1 + 1 \> 7|[1] j!1 \> 7\n[2] EXIST (t : nat, f : nat) : j!1 + 1 = 3 * t + 5 * f}" | + | label = "{[-1] j!1 = 7\n[-2] j!1 + 1 \> 7|[1] j!1 \> 7\n[2] EXIST (t : nat, f : nat) : j!1 + 1 = 3 * t + 5 * f}" |
shape = "record" | shape = "record" | ||
] | ] | ||
- | " | + | "node35" -> "node36" |
"node37" [ | "node37" [ | ||
- | label = "( | + | label = "(inst 2 \"1\" \"1\")" |
] | ] | ||
"node36" -> "node37" | "node36" -> "node37" | ||
"node38" [ | "node38" [ | ||
- | label = "{[-1] j!1 = 7\n[-2] j!1 + 1 \> 7|[1] j!1 \> 7\n[2] | + | label = "{[-1] j!1 = 7\n[-2] j!1 + 1 \> 7|[1] j!1 \> 7\n[2] j!1 + 1 = 3 * 1 + 5 * 1}" |
shape = "record" | shape = "record" | ||
] | ] | ||
"node37" -> "node38" | "node37" -> "node38" | ||
"node39" [ | "node39" [ | ||
- | label = "( | + | label = "(assert)" |
+ | style = "filled" | ||
+ | fillcolor = "green" | ||
] | ] | ||
"node38" -> "node39" | "node38" -> "node39" | ||
"node40" [ | "node40" [ | ||
- | label = "{[-1] j!1 = 7\n[-2] j!1 + 1 \> 7|[1] j!1 \> 7\n[2] j!1 + 1 = 3 * | + | label = "{[-1] j!1 /= 7\n[-2] j!1 + 1 \> 7|[1] j!1 \> 7\n[2] EXIST (t : nat, f : nat) : j!1 + 1 = 3 * t + 5 * f}" |
shape = "record" | shape = "record" | ||
] | ] | ||
- | " | + | "node35" -> "node40" |
"node41" [ | "node41" [ | ||
label = "(assert)" | label = "(assert)" | ||
Строка 195: | Строка 206: | ||
] | ] | ||
"node40" -> "node41" | "node40" -> "node41" | ||
- | "node42" [ | ||
- | label = "{[-1] j!1 + 1 \> 7|[1] j!1 = 7\n[2] j!1 \> 7\n[3] EXIST (t : nat, f : nat) : j!1 + 1 = 3 * t + 5 * f}" | ||
- | shape = "record" | ||
- | ] | ||
- | "node37" -> "node42" | ||
- | "node43" [ | ||
- | label = "(assert)" | ||
- | style = "filled" | ||
- | fillcolor = "green" | ||
- | ] | ||
- | "node42" -> "node43" | ||
} | } | ||
</pre> | </pre> |