+
+
+Components $M$ and $M'$ obey, respectively, contracts $C = (|i| \le 2, o \le i \le 2o + 2)$ and $C' = (-1 \le o \le 1/5, o' \le o)$. We can use Pacti to obtain the specification of the system by executing the command
+
+`pacti examples/example.json result.json`
+
+Pacti places the result of composition in the file result.json. The output is
+
+```
+ Composed contract:
+ InVars: []
+ OutVars:[]
+ A: 5*i <= 1, -1/2*i <= 0
+ G: -1*i + 1*o_p <= 0
+```
+
+### Quotient
+
+
+Now we consider an example of quotient. Consider the following circuits:
+
+
+
+We wish to implement a system $M$ with specification $C = (|i| \le 1, o' = 2i + 1)$, and to do this we have available a component $M'$ with specification $C' = (|i| \le 2, o = 2i)$. We use the quotient operation in Pacti to obtain the specification of the component that we are missing so that the resulting object meets the specification $C$. We run the command
+
+`pacti examples/example_quotient.json result.json`
+
+And Pacti outputs
+
+```
+ Contract quotient:
+ InVars: []
+ OutVars:[]
+ A: 1*o <= 2, -1*o <= 2
+ G: -1*o + 1*o_p <= 1, 1*o + -1*o_p <= -1
+```
\ No newline at end of file
diff --git a/docs/css/material.css b/docs/css/material.css
index 9e8c14a6..b5fb7fbf 100644
--- a/docs/css/material.css
+++ b/docs/css/material.css
@@ -2,3 +2,8 @@
.md-main__inner {
margin-bottom: 1.5rem;
}
+
+
+.md-content__button {
+ display: none;
+}
\ No newline at end of file
diff --git a/docs/getting_started.ipynb b/docs/getting_started.ipynb
new file mode 100644
index 00000000..aa30b04d
--- /dev/null
+++ b/docs/getting_started.ipynb
@@ -0,0 +1,251 @@
+{
+ "cells": [
+ {
+ "attachments": {},
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "# Getting started\n",
+ "\n",
+ "Pacti helps designers to reason about specifications and to manipulate them. These specifications are given to Pacti as assume-guarantee contracts, which are requirements of the form (assumptions, guarantees).\n",
+ "\n",
+ "For Pacti, every contract has four elements:\n",
+ "- Input variables\n",
+ "- Output variables\n",
+ "- Assumptions\n",
+ "- Guarantees\n",
+ "\n",
+ "The assumptions of a contract are only allowed to refer to the input variables. Guarantees are only allowed to refer to the input and output variables of the contract, i.e., no variables outside the interface of the contract may appear in the assumptions or guarantees.\n",
+ "\n",
+ "The algebra of contracts has been extensively researched. This algebra allows us to compute new specifications from existing contracts. For example,\n",
+ "- The operation of composition allows us to compute the specification of the system formed by composing subsystems obeying the specifications being composed. In other words, composition is the system-building operation.\n",
+ "- The operation of quotient allows us to compute the specification of a component that needs to be composed with an existing subsystem so that the resulting system meets a top-level specification. Quotient is used to find missing-component specifications.\n",
+ "- The operation of merging is used to generate a single contract that simultaneously enforces the assumptions and guarantees of the contracts being merged. This is used to fuse contract viewpoints in concurrent design.\n",
+ "\n",
+ "### Computing system specifications\n",
+ "\n",
+ "\n",
+ "Consider the following system:\n",
+ "\n",
+ "\n",
+ "\n",
+ "Components $M$ and $M'$ obey, respectively, contracts $C = (|i| \\le 2, o \\le i \\le 2o + 2)$ and $C' = (-1 \\le o \\le 1/5, o' \\le o)$. We can use Pacti to obtain the specification of the system that comprises these two components as follows: "
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 3,
+ "metadata": {},
+ "outputs": [
+ {
+ "name": "stdout",
+ "output_type": "stream",
+ "text": [
+ "InVars: [i]\n",
+ "OutVars:[o_p]\n",
+ "A: [\n",
+ " i <= 0.19999999999999996\n",
+ " -0.5 i <= 0.0\n",
+ "]\n",
+ "G: [\n",
+ " -i + o_p <= 0.0\n",
+ "]\n"
+ ]
+ }
+ ],
+ "source": [
+ "from pacti.terms.polyhedra import PolyhedralContract\n",
+ "\n",
+ "contract1 = PolyhedralContract.from_string(\n",
+ " InputVars=[\"i\"],\n",
+ " OutputVars=[\"o\"],\n",
+ " assumptions=[\"|i| <= 2\"],\n",
+ " guarantees=[\"o - i <= 0\", \"i - 2o <= 2\"])\n",
+ "\n",
+ "contract2 = PolyhedralContract.from_string(\n",
+ " InputVars=[\"o\"],\n",
+ " OutputVars=[\"o_p\"],\n",
+ " assumptions=[\"o <= 0.2\", \"-o <= 1\"],\n",
+ " guarantees=[\"o_p - o <= 0\"])\n",
+ "\n",
+ "system_contract = contract1.compose(contract2)\n",
+ "print(system_contract)"
+ ]
+ },
+ {
+ "attachments": {},
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "Pacti gives us the specification of the system. Note that the resulting contract only involves the top-level inputs and outputs.\n",
+ "\n",
+ "\n",
+ "### System diagnostics\n",
+ "\n",
+ "Suppose that we are trying to build a system as shown in the figure above with the same specification $C'$ for $M'$. Suppose that now the specification $C_n$ for $M$ is $(|i| <= 2, |o| <= 3)$."
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 4,
+ "metadata": {},
+ "outputs": [
+ {
+ "ename": "ValueError",
+ "evalue": "The guarantees \n[\n |o| <= 3.0\n]\nwere insufficient to abduce the assumptions \n[\n o <= 0.2\n -o <= 1.0\n]\nby eliminating the variables \n[, ]",
+ "output_type": "error",
+ "traceback": [
+ "\u001b[1;31m---------------------------------------------------------------------------\u001b[0m",
+ "\u001b[1;31mValueError\u001b[0m Traceback (most recent call last)",
+ "Cell \u001b[1;32mIn[4], line 7\u001b[0m\n\u001b[0;32m 1\u001b[0m contract1_n \u001b[39m=\u001b[39m PolyhedralContract\u001b[39m.\u001b[39mfrom_string(\n\u001b[0;32m 2\u001b[0m InputVars\u001b[39m=\u001b[39m[\u001b[39m\"\u001b[39m\u001b[39mi\u001b[39m\u001b[39m\"\u001b[39m],\n\u001b[0;32m 3\u001b[0m OutputVars\u001b[39m=\u001b[39m[\u001b[39m\"\u001b[39m\u001b[39mo\u001b[39m\u001b[39m\"\u001b[39m],\n\u001b[0;32m 4\u001b[0m assumptions\u001b[39m=\u001b[39m[\u001b[39m\"\u001b[39m\u001b[39m|i| <= 2\u001b[39m\u001b[39m\"\u001b[39m],\n\u001b[0;32m 5\u001b[0m guarantees\u001b[39m=\u001b[39m[\u001b[39m\"\u001b[39m\u001b[39m|o| <= 3\u001b[39m\u001b[39m\"\u001b[39m])\n\u001b[1;32m----> 7\u001b[0m contract_system \u001b[39m=\u001b[39m contract1_n\u001b[39m.\u001b[39;49mcompose(contract2)\n",
+ "File \u001b[1;32m~\\iir_repo\\pacti\\src\\pacti\\iocontract\\iocontract.py:458\u001b[0m, in \u001b[0;36mIoContract.compose\u001b[1;34m(self, other)\u001b[0m\n\u001b[0;32m 456\u001b[0m new_a \u001b[39m=\u001b[39m other\u001b[39m.\u001b[39ma\u001b[39m.\u001b[39mabduce_with_context(\u001b[39mself\u001b[39m\u001b[39m.\u001b[39ma \u001b[39m|\u001b[39m \u001b[39mself\u001b[39m\u001b[39m.\u001b[39mg, assumptions_forbidden_vars)\n\u001b[0;32m 457\u001b[0m \u001b[39mif\u001b[39;00m list_intersection(new_a\u001b[39m.\u001b[39mvars, assumptions_forbidden_vars):\n\u001b[1;32m--> 458\u001b[0m \u001b[39mraise\u001b[39;00m \u001b[39mValueError\u001b[39;00m(\n\u001b[0;32m 459\u001b[0m \u001b[39m\"\u001b[39m\u001b[39mThe guarantees \u001b[39m\u001b[39m\\n\u001b[39;00m\u001b[39m{}\u001b[39;00m\u001b[39m\\n\u001b[39;00m\u001b[39m\"\u001b[39m\u001b[39m.\u001b[39mformat(\u001b[39mself\u001b[39m\u001b[39m.\u001b[39mg)\n\u001b[0;32m 460\u001b[0m \u001b[39m+\u001b[39m \u001b[39m\"\u001b[39m\u001b[39mwere insufficient to abduce the assumptions \u001b[39m\u001b[39m\\n\u001b[39;00m\u001b[39m{}\u001b[39;00m\u001b[39m\\n\u001b[39;00m\u001b[39m\"\u001b[39m\u001b[39m.\u001b[39mformat(other\u001b[39m.\u001b[39ma)\n\u001b[0;32m 461\u001b[0m \u001b[39m+\u001b[39m \u001b[39m\"\u001b[39m\u001b[39mby eliminating the variables \u001b[39m\u001b[39m\\n\u001b[39;00m\u001b[39m{}\u001b[39;00m\u001b[39m\"\u001b[39m\u001b[39m.\u001b[39mformat(assumptions_forbidden_vars)\n\u001b[0;32m 462\u001b[0m )\n\u001b[0;32m 463\u001b[0m assumptions \u001b[39m=\u001b[39m new_a \u001b[39m|\u001b[39m \u001b[39mself\u001b[39m\u001b[39m.\u001b[39ma\n\u001b[0;32m 464\u001b[0m \u001b[39melif\u001b[39;00m other_helps_self \u001b[39mand\u001b[39;00m \u001b[39mnot\u001b[39;00m self_helps_other:\n",
+ "\u001b[1;31mValueError\u001b[0m: The guarantees \n[\n |o| <= 3.0\n]\nwere insufficient to abduce the assumptions \n[\n o <= 0.2\n -o <= 1.0\n]\nby eliminating the variables \n[, ]"
+ ]
+ }
+ ],
+ "source": [
+ "contract1_n = PolyhedralContract.from_string(\n",
+ " InputVars=[\"i\"],\n",
+ " OutputVars=[\"o\"],\n",
+ " assumptions=[\"|i| <= 2\"],\n",
+ " guarantees=[\"|o| <= 3\"])\n",
+ "\n",
+ "contract_system = contract1_n.compose(contract2)"
+ ]
+ },
+ {
+ "attachments": {},
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "Pacti is unable to compute a system specification. In this case, this is due to the fact that our guarantee $|o| \\le 3$ for $M$ does not satisfy the assumptions of $C'$."
+ ]
+ },
+ {
+ "attachments": {},
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "### Quotient\n",
+ "\n",
+ "Now consider the situation shown in the following diagram:\n",
+ "\n",
+ ""
+ ]
+ },
+ {
+ "attachments": {},
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "We wish to implement a system $M$ with specification $C = (|i| \\le 1, o' = 2i + 1)$, and to do this we have available a component $M'$ with specification $C' = (|i| \\le 2, o = 2i)$. We use the quotient operation in Pacti to obtain the specification of the component that we are missing--that would fill the question mark--so that the resulting object meets the specification $C$."
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 5,
+ "metadata": {},
+ "outputs": [
+ {
+ "name": "stdout",
+ "output_type": "stream",
+ "text": [
+ "InVars: [o]\n",
+ "OutVars:[o_p]\n",
+ "A: [\n",
+ " |o| <= 2.0\n",
+ "]\n",
+ "G: [\n",
+ " -o + o_p = 1.0\n",
+ "]\n"
+ ]
+ }
+ ],
+ "source": [
+ "contract_top_level = PolyhedralContract.from_string(\n",
+ " InputVars=[\"i\"],\n",
+ " OutputVars=[\"o_p\"],\n",
+ " assumptions=[\"|i| <= 1\"],\n",
+ " guarantees=[\"o_p - 2i = 1\"])\n",
+ "\n",
+ "contract_existing_component = PolyhedralContract.from_string(\n",
+ " InputVars=[\"i\"],\n",
+ " OutputVars=[\"o\"],\n",
+ " assumptions=[\"|i| <= 2\"],\n",
+ " guarantees=[\"o - 2i = 0\"])\n",
+ "\n",
+ "contract_missing_object = contract_top_level.quotient(contract_existing_component)\n",
+ "print(contract_missing_object)"
+ ]
+ },
+ {
+ "attachments": {},
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "Observe that Pacti tells us that the missing component's specification has input $o$ and output $o'$. The resulting specification is guaranteed to implement the top-level system when composed with the contract of the existing component. We can verify this:"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 6,
+ "metadata": {},
+ "outputs": [
+ {
+ "name": "stdout",
+ "output_type": "stream",
+ "text": [
+ "True\n"
+ ]
+ }
+ ],
+ "source": [
+ "# compose quotient \n",
+ "new_system_object = contract_missing_object.compose(contract_existing_component)\n",
+ "print(new_system_object.refines(contract_top_level))"
+ ]
+ },
+ {
+ "attachments": {},
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "### To learn more\n",
+ "\n",
+ "These introductory examples show some analysis tasks we can carry out with Pacti. The `case_studies` folder contains several case studies that discuss the application of Pacti in various design disciplines."
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": []
+ }
+ ],
+ "metadata": {
+ "kernelspec": {
+ "display_name": ".venv",
+ "language": "python",
+ "name": "python3"
+ },
+ "language_info": {
+ "codemirror_mode": {
+ "name": "ipython",
+ "version": 3
+ },
+ "file_extension": ".py",
+ "mimetype": "text/x-python",
+ "name": "python",
+ "nbconvert_exporter": "python",
+ "pygments_lexer": "ipython3",
+ "version": "3.10.7"
+ },
+ "orig_nbformat": 4,
+ "vscode": {
+ "interpreter": {
+ "hash": "b282b3e35ff361393169c4f355db145ffcb63e574f57c9818c827b7c99ca9fc3"
+ }
+ }
+ },
+ "nbformat": 4,
+ "nbformat_minor": 2
+}
diff --git a/docs/index.md b/docs/index.md
index ec08973e..52ce6657 100644
--- a/docs/index.md
+++ b/docs/index.md
@@ -10,48 +10,4 @@ system using assume-guarantee specifications, or contracts. Pacti's capabilities
- Computing specifications of subsystems that need to be added to a design in order to meet an objective.
- Verifying whether a component meets a specification.
-## Examples
-
-### Composition
-
-
-Suppose we have the following system:
-
-
-
-
-Components $M$ and $M'$ obey, respectively, contracts $C = (|i| \le 2, o \le i \le 2o + 2)$ and $C' = (-1 \le o \le 1/5, o' \le o)$. We can use Pacti to obtain the specification of the system by executing the command
-
-`pacti examples/example.json result.json`
-
-Pacti places the result of composition in the file result.json. The output is
-
-```
- Composed contract:
- InVars: []
- OutVars:[]
- A: 5*i <= 1, -1/2*i <= 0
- G: -1*i + 1*o_p <= 0
-```
-
-### Quotient
-
-
-Now we consider an example of quotient. Consider the following circuits:
-
-
-
-We wish to implement a system $M$ with specification $C = (|i| \le 1, o' = 2i + 1)$, and to do this we have available a component $M'$ with specification $C' = (|i| \le 2, o = 2i)$. We use the quotient operation in Pacti to obtain the specification of the component that we are missing so that the resulting object meets the specification $C$. We run the command
-
-`pacti examples/example_quotient.json result.json`
-
-And Pacti outputs
-
-```
- Contract quotient:
- InVars: []
- OutVars:[]
- A: 1*o <= 2, -1*o <= 2
- G: -1*o + 1*o_p <= 1, 1*o + -1*o_p <= -1
-```
diff --git a/docs/getting_started.md b/docs/installing.md
similarity index 100%
rename from docs/getting_started.md
rename to docs/installing.md
diff --git a/docs/source/_static/circuit_series_composition_background.ai b/docs/source/_static/circuit_series_composition_background.ai
new file mode 100644
index 00000000..1bbd6782
--- /dev/null
+++ b/docs/source/_static/circuit_series_composition_background.ai
@@ -0,0 +1,1586 @@
+%PDF-1.6
%
+1 0 obj
<>/OCGs[23 0 R]>>/Pages 3 0 R/Type/Catalog>>
endobj
2 0 obj
<>stream
+
+