From 837a8cc320ffef15029229d99603fd54889f17b7 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Liam=20O=E2=80=99Connor?= Date: Wed, 22 Jul 2026 15:23:27 +1000 Subject: [PATCH] add itp notes --- test.lua | 10 ++++++++++ trees/ltp/ltp-0001.tree | 8 ++++++++ trees/ltp/ltp-000X.tree | 8 ++++++++ trees/ltp/ltp-000Y.tree | 15 +++++++++++++++ trees/ltp/ltp-000Z.tree | 17 +++++++++++++++++ trees/ltp/ltp-0010.tree | 7 +++++++ trees/ltp/ltp-0011.tree | 13 +++++++++++++ trees/people/manna.tree | 6 ++++++ trees/people/pnueli.tree | 5 +++++ trees/places/podc90.tree | 6 ++++++ trees/places/stanford.tree | 4 ++++ trees/refs/manna-pnueli-1990.tree | 8 ++++++++ 12 files changed, 107 insertions(+) create mode 100644 test.lua create mode 100644 trees/ltp/ltp-000X.tree create mode 100644 trees/ltp/ltp-000Y.tree create mode 100644 trees/ltp/ltp-000Z.tree create mode 100644 trees/ltp/ltp-0010.tree create mode 100644 trees/ltp/ltp-0011.tree create mode 100644 trees/people/manna.tree create mode 100644 trees/people/pnueli.tree create mode 100644 trees/places/podc90.tree create mode 100644 trees/places/stanford.tree create mode 100644 trees/refs/manna-pnueli-1990.tree diff --git a/test.lua b/test.lua new file mode 100644 index 0000000..0c3d83b --- /dev/null +++ b/test.lua @@ -0,0 +1,10 @@ +vim.filetype.add({ extension = { tree = "forester" } }) + +vim.cmd("edit trees/index.tree") + +local client_id = vim.lsp.start({ + name = "forester-lsp", + cmd = { "forester", "lsp" }, + root_dir = vim.fs.root(0, { "forest.toml" }), +}) + diff --git a/trees/ltp/ltp-0001.tree b/trees/ltp/ltp-0001.tree index c511f72..11965e8 100644 --- a/trees/ltp/ltp-0001.tree +++ b/trees/ltp/ltp-0001.tree @@ -48,3 +48,11 @@ \transclude{ltp-000V} \transclude{ltp-000W} } +\subtree{ + \title{Concerning decision properties} + \scope{\put\transclude/metadata{true}\transclude{ltp-000X}} + \transclude{ltp-000Y} + \transclude{ltp-000Z} + \transclude{ltp-0010} +} + \scope{\put\transclude/metadata{true}\transclude{ltp-0011}} diff --git a/trees/ltp/ltp-000X.tree b/trees/ltp/ltp-000X.tree new file mode 100644 index 0000000..ccada9b --- /dev/null +++ b/trees/ltp/ltp-000X.tree @@ -0,0 +1,8 @@ +\import{dt-macros} +\import{ltp-macros} +\title{Decision properties} +\taxon{Definition} +%\author{liamoc} +\meta{source}{(from [[amjad-vanglabbeek-oconnor-2026]])} +\p{A \em{decision} property (called \em{strong monitorable} by [Amjad et al.](amjad-vanglabbeek-oconnor-2026)) is a [property](ltp-0003) for which \em{both} confirmation and refutation only require a finite prefix. In other words, decision properties are the intersection of a [safety](ltp-0004) and [guarantee](ltp-0005) property. +This makes decision properties the clopen sets in our [topology](ltp-0007). A simple characterisation from topology is that #{P} is a decision property iff #{\sc{P}=\gk{P}}.} \ No newline at end of file diff --git a/trees/ltp/ltp-000Y.tree b/trees/ltp/ltp-000Y.tree new file mode 100644 index 0000000..6fe3f51 --- /dev/null +++ b/trees/ltp/ltp-000Y.tree @@ -0,0 +1,15 @@ +\import{dt-macros} +\import{ltp-macros} +\taxon{Theorem} +\author{liamoc} +\title{Decision properties are closed under complement} +\p{If #{P} is a [decision property](ltp-000X) then so is #{\compl{P}}.} +\proofblock{ + \p{ + We know that #{\sc{P}=\gk{P}}. Then, from the definition of [safety closure](ltp-000J), we have:: + ##{\begin{array}{lcl} + \sc{\compl{P}} & = & \compl{\gk{P}} \\ + & = & \compl{\sc{P}} \\ + & = & \gk{\compl{P}}\end{array}} + } +} \ No newline at end of file diff --git a/trees/ltp/ltp-000Z.tree b/trees/ltp/ltp-000Z.tree new file mode 100644 index 0000000..9324a3f --- /dev/null +++ b/trees/ltp/ltp-000Z.tree @@ -0,0 +1,17 @@ +\import{dt-macros} +\import{ltp-macros} +\taxon{Theorem} +\author{liamoc} +\title{Decision properties are closed under finite union and intersection} +\p{If #{P} and #{Q} are [decision properties](ltp-000X) then so is #{P \cup Q} and #{P \cap Q}.} +\proofblock{ + \p{ + We know that #{\sc{P}=\gk{P}} and #{\sc{Q}=\gk{Q}}. As [safety closure distributes over finite union](ltp-000Q) and the [guarantee kernel is monotonic](ltp-000I), we have: + ##{\begin{array}{lcl} + \sc{P \cup Q} & = & \sc{P} \cup \sc{Q} \\ + & = & \gk{P} \cup \gk{Q} \\ + & \subseteq & \gk{P \cup Q} \\ + & \subseteq & \sc{P \cup Q} \end{array}} + } + As the inclusion ends up again at #{\sc{P\cup Q}}, the inclusions must be equalities, and thus #{\sc{P \cup Q} = \gk{P \cup Q}}. As [decision properties are closed under complement](ltp-000Y), the proof for intersection follows from this straightforwardly. +} \ No newline at end of file diff --git a/trees/ltp/ltp-0010.tree b/trees/ltp/ltp-0010.tree new file mode 100644 index 0000000..45306db --- /dev/null +++ b/trees/ltp/ltp-0010.tree @@ -0,0 +1,7 @@ +\import{dt-macros} +\import{ltp-macros} +\taxon{Counterexample} +\title{Decision properties are not closed under infinite union nor intersection} +\author{liamoc} +\p{Follows from \ref{ltp-000E}. Each #{P_i} is both a [safety property](ltp-0004) and a [guarantee property](ltp-0005). Therefore, each #{P_i} is a [decision property](ltp-000X). But the [safety closure](ltp-000J) of their infinite union #{\bigcup_{i \in \mathbb{N}} P_i} is the strictly larger set #{\itraces}. Therefore, their infinite union is not even a [safety property](ltp-0004) so certainly not a [decision property](ltp-000X).} +\p{Therefore, decision properties are not closed under infinite union. Because [decision properties are closed under complement](ltp-000Y), they cannot be closed under infinite intersection either.} \ No newline at end of file diff --git a/trees/ltp/ltp-0011.tree b/trees/ltp/ltp-0011.tree new file mode 100644 index 0000000..c96eac6 --- /dev/null +++ b/trees/ltp/ltp-0011.tree @@ -0,0 +1,13 @@ +\import{dt-macros} +\import{ltp-macros} +\title{Obligation properties} +\taxon{Definition} +\meta{source}{(from [[manna-pnueli-1990]])} +\p{An \em{obligation} property is comprised of (finite) boolean combinations of [safety](ltp-0004) and [guarantee](ltp-0005) properties. That is:} +\ul{ +\li{Every [guarantee](ltp-0004) property is an obligation property.} +\li{If #{P} is an obligation property, then #{\compl{P}} is an obligation property.} +\li{If #{P} and #{Q} are obligation properties, then #{P \cap Q} is an obligation property.} +\li{If #{P} and #{Q} are obligation properties, then #{P \cup Q} is an obligation property.} +} +\p{Topologically, this is called the \em{constructible sets} of our [topology](ltp-0007).} \ No newline at end of file diff --git a/trees/people/manna.tree b/trees/people/manna.tree new file mode 100644 index 0000000..d02905b --- /dev/null +++ b/trees/people/manna.tree @@ -0,0 +1,6 @@ +\title{Zohar Manna} +\taxon{Person} +\meta{position}{Professor (deceased)} +\meta{external}{https://en.wikipedia.org/wiki/Zohar_Manna} +\meta{institution}{[[stanford]]} + diff --git a/trees/people/pnueli.tree b/trees/people/pnueli.tree new file mode 100644 index 0000000..ca694d4 --- /dev/null +++ b/trees/people/pnueli.tree @@ -0,0 +1,5 @@ +\title{Amir Pnueli} +\taxon{Person} +\meta{position}{Professor (deceased)} +\meta{external}{https://en.wikipedia.org/wiki/Amir_Pnueli} + diff --git a/trees/places/podc90.tree b/trees/places/podc90.tree new file mode 100644 index 0000000..a47185e --- /dev/null +++ b/trees/places/podc90.tree @@ -0,0 +1,6 @@ +\import{conf-name-macros} +\taxon{Conference} +\meta{doi}{10.1145/93385} +\title{\conf-name{PODC '90}{Ninth Annual ACM Symposium on Principles of Distributed Computing}} +\date{1990-08} +\meta{venue}{Quebec City, Quebec, Canada} \ No newline at end of file diff --git a/trees/places/stanford.tree b/trees/places/stanford.tree new file mode 100644 index 0000000..a48ec9c --- /dev/null +++ b/trees/places/stanford.tree @@ -0,0 +1,4 @@ +\title{Stanford University} +\taxon{Institution} +\meta{venue}{California, USA} +\meta{external}{https://www.stanford.edu/} diff --git a/trees/refs/manna-pnueli-1990.tree b/trees/refs/manna-pnueli-1990.tree new file mode 100644 index 0000000..f594203 --- /dev/null +++ b/trees/refs/manna-pnueli-1990.tree @@ -0,0 +1,8 @@ +\author{manna} +\author{pnueli} +\taxon{Reference} +\meta{venue}{[[podc90]]} +\tag{refereed} +\date{1990-08-01} +\meta{doi}{10.1145/93385.93442} +\title{A Hierarchy of Temporal Properties} \ No newline at end of file -- 2.51.2