Skip to content

Commit

Permalink
cleanup table
Browse files Browse the repository at this point in the history
  • Loading branch information
@pauleve
pauleve committed May 9, 2024
1 parent a35d4b4 commit 03c7ef1
Show file tree
Hide file tree
Showing 3 changed files with 92 additions and 62 deletions.
27 changes: 27 additions & 0 deletions _static/style.css
View file
Original file line number Diff line number Diff line change
Expand Up @@ -5,3 +5,30 @@ p.footer img.logo {
p.footer img.logo-labri {
padding: 1%;
}

table.language {
margin-left: 0 !important;
margin-right: auto !important;
}
table.language td {
padding: 0px 8px;
}
table.language > tbody > tr > td:first-of-type {
border-right: 1px solid;
}
table.language > tbody > tr:nth-of-type(even) {
background-color: var(--pst-color-surface);
}

.obs {
color: var(--pst-color-accent);
}
.cfg {
color: var(--pst-color-primary);
}
.some {
color: var(--pst-color-secondary);
}
.bokey {
color: var(--pst-color-primary-highlight);
}
125 changes: 64 additions & 61 deletions language.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -6,41 +6,41 @@ In the scope of a `BoNesis(dom, data)`{l=python} object, the following methods a

### Objects

#### <span style="color:purple">Observation</span>:
#### <span class="obs">Observation</span>:
maps a subset of components to a Boolean value

<table style="margin-left: 0 !important; margin-right: auto !important;">
<table class="language">
<tr>
<td style="padding: 0px 8px; border-right: 1px solid black;"><code><span style="color:purple">O</span> = obs({<span style="color:olive">a</span>:0, <span style="color:olive">b</span>:1,..})</code></td>
<td style="padding: 0px 8px;">Observation from partial mapping of components to <code>0</code> or <code>1</code> (<code>dict</code>-like object)</td>
<td><code><span class="obs">O</span> = obs({<span class="bokey">a</span>:0, <span class="bokey">b</span>:1,..})</code></td>
<td>Observation from partial mapping of components to <code>0</code> or <code>1</code> (<code>dict</code>-like object)</td>
</tr>
<tr style="background-color: #EEEEEE;">
<td style="padding: 0px 8px; border-right: 1px solid black;"><code><span style="color:purple">O</span> = obs("name")</code></td>
<td style="padding: 0px 8px;">Named observation defined in the <code>data</code> dictionary</td>
<tr>
<td><code><span class="obs">O</span> = obs("name")</code></td>
<td><code>data</code> dictionary</td>
</tr>
</table>


#### <span style="color:blue">Configuration</span>:
#### <span class="cfg">Configuration</span>:
maps each component to a Boolean value

<table style="margin-left: 0 !important; margin-right: auto !important;">
<table class="language">
<tr>
<td style="padding: 0px 8px; border-right: 1px solid black;"><code><span style="color:blue">C</span> = cfg()</code></td>
<td style="padding: 0px 8px;">Allocates a fresh configuration</td>
<td><code><span class="cfg">C</span> = cfg()</code></td>
<td>Allocates a fresh configuration</td>
</tr>
<tr style="background-color: #EEEEEE;">
<td style="padding: 0px 8px; border-right: 1px solid black;"><code><span style="color:blue">C</span> = +<span style="color:purple">O</span></code></td>
<td style="padding: 0px 8px;">Fresh configuration matching with the observation <code><span style="color:purple">O</span></code></td>
<tr>
<td><code><span class="cfg">C</span> = +<span class="obs">O</span></code></td>
<td>Fresh configuration matching with the observation <code><span class="obs">O</span></code></td>
</tr>
<tr style="border-bottom: 1px solid black;">
<td style="padding: 0px 8px; border-right: 1px solid black;"><code><span style="color:blue">C</span> = ~<span style="color:purple">O</span></code></td>
<td style="padding: 0px 8px;">Default configuration matching with the observation <code><span style="color:purple">O</span></code></td>
<tr>
<td><code><span class="cfg">C</span> = ~<span class="obs">O</span></code></td>
<td>Default configuration matching with the observation <code><span class="obs">O</span></code></td>
</tr>
<tr style="background-color: #EEEEEE;">
<td style="padding: 0px 8px; border-right: 1px solid black;"><code><span style="color:green">S</span> = Some(max_size=k)</code></td>
<td style="padding: 0px 8px;">Represents a mutation of at most <code>k</code> components.<br/>
Use <code><span style="color:green">S</span>.assignments()</code> to get satisfying valuations.</td>
<tr>
<td><code><span class="some">S</span> = Some(max_size=k)</code></td>
<td>Represents a mutation of at most <code>k</code> components.<br/>
Use <code><span class="some">S</span>.assignments()</code> to get satisfying valuations.</td>
</tr>
</table>

Expand All @@ -49,89 +49,92 @@ maps each component to a Boolean value

#### Constraints on configurations

<table style="margin-left: 0 !important; margin-right: auto !important;">
<table class="language">
<tr>
<td style="padding: 0px 8px; border-right: 1px solid black;"><code><span style="color:blue">C</span> != <span style="color:blue">C'</span></code></td>
<td style="padding: 0px 8px;">The configurations <code><span style="color:blue">C</span></code> and <code><span style="color:blue">C'</span></code> differ on at least one component</td>
<td><code><span class="cfg">C</span> != <span class="cfg">C'</span></code></td>
<td>The configurations <code><span class="cfg">C</span></code> and <code><span class="cfg">C'</span></code> differ on at least one component</td>
</tr>
<tr style="background-color: #EEEEEE;">
<td style="padding: 0px 8px; border-right: 1px solid black;"><nobr><code><span style="color:blue">C</span>[<span style="color:olive">a</span>] == <span style="color:blue">C'</span>[<span style="color:olive">b</span>] <span style="color:gray">|</span> 0 <span style="color:gray">|</span> 1</code></nobr><br/>
<nobr><code><span style="color:blue">C</span>[<span style="color:olive">a</span>] != <span style="color:blue">C'</span>[<span style="color:olive">b</span>] <span style="color:gray">|</span> 0 <span style="color:gray">|</span> 1</code></nobr></td>
<td style="padding: 0px 8px;">The state of the component <code><span style="color:olive">a</span></code> in the configuration <code><span style="color:blue">C</span></code> is equal (resp. different) to the state of the component <code><span style="color:olive">b</span></code> in the configuration <code><span style="color:blue">C'</span></code> (resp. 0 and 1)</td>
<tr>
<td><nobr><code><span class="cfg">C</span>[<span class="bokey">a</span>] == <span class="cfg">C'</span>[<span class="bokey">b</span>] <span style="color:gray">|</span> 0 <span style="color:gray">|</span> 1</code></nobr><br/>
<td rowspan="2">The state of the component <code><span class="bokey">a</span></code> in the configuration <code><span class="cfg">C</span></code> is equal (resp. different) to the state of the component <code><span class="bokey">b</span></code> in the configuration <code><span class="cfg">C'</span></code> (resp. 0 and 1)</td>
</tr>
<tr>
<td>
<nobr><code><span class="cfg">C</span>[<span class="bokey">a</span>] != <span class="cfg">C'</span>[<span class="bokey">b</span>] <span style="color:gray">|</span> 0 <span style="color:gray">|</span> 1</code></nobr></td>
</tr>
<tr>
<td style="padding: 0px 8px; border-right: 1px solid black;"><code><span style="color:blue">C</span> != <span style="color:purple">O</span></code></td>
<td style="padding: 0px 8px;">The configuration <code><span style="color:blue">C</span></code> does not match with the observation <code><span style="color:purple">O</span></code></td>
<td><code><span class="cfg">C</span> != <span class="obs">O</span></code></td>
<td>The configuration <code><span class="cfg">C</span></code> does not match with the observation <code><span class="obs">O</span></code></td>
</tr>
</table>


#### Attractor properties

<table style="margin-left: 0 !important; margin-right: auto !important;">
<table class="language">
<tr>
<td style="padding: 0px 8px; border-right: 1px solid black;"><code>fixed(<span style="color:blue">C</span>)</code></td>
<td style="padding: 0px 8px;">The configuration <code><span style="color:blue">C</span></code> is a fixed point</td>
<td><code>fixed(<span class="cfg">C</span>)</code></td>
<td>The configuration <code><span class="cfg">C</span></code> is a fixed point</td>
</tr>
<tr style="background-color: #EEEEEE;">
<td style="padding: 0px 8px; border-right: 1px solid black;"><code>fixed(<span style="color:purple">O</span>)</code></td>
<td style="padding: 0px 8px;">There exists a trap space where observation <code><span style="color:purple">O</span></code> is fixed</td>
<tr>
<td><code>fixed(<span class="obs">O</span>)</code></td>
<td>There exists a trap space where observation <code><span class="obs">O</span></code> is fixed</td>
</tr>
<tr>
<td style="padding: 0px 8px; border-right: 1px solid black;"><code>in_attractor(<span style="color:blue">C</span>)</code></td>
<td style="padding: 0px 8px;">The configuration <code><span style="color:blue">C</span></code> belongs to an attractor</td>
<td><code>in_attractor(<span class="cfg">C</span>)</code></td>
<td>The configuration <code><span class="cfg">C</span></code> belongs to an attractor</td>
</tr>
</table>


#### Reachability

<table style="margin-left: 0 !important; margin-right: auto !important;">
<table class="language">
<tr>
<td style="padding: 0px 8px; border-right: 1px solid black;"><code><span style="color:blue">C</span> >= <span style="color:blue">C'</span></code> or <code>reach(<span style="color:blue">C</span>,<span style="color:blue">C'</span>)</code></td>
<td style="padding: 0px 8px;">There exists an MP trajectory from the configuration <code><span style="color:blue">C</span></code> to the configuration <code><span style="color:blue">C'</span></code></td>
<td><code><span class="cfg">C</span> >= <span class="cfg">C'</span></code> or <code>reach(<span class="cfg">C</span>,<span class="cfg">C'</span>)</code></td>
<td>There exists an MP trajectory from the configuration <code><span class="cfg">C</span></code> to the configuration <code><span class="cfg">C'</span></code></td>
</tr>
<tr style="background-color: #EEEEEE;">
<td style="padding: 0px 8px; border-right: 1px solid black;"><code><span style="color:blue">C</span> >= <span style="color:purple">O</span></code></td>
<td style="padding: 0px 8px;">... to a configuration matching with the observation <code><span style="color:purple">O</span></code> (equiv to <code><span style="color:blue">C</span> >= +<span style="color:purple">O</span></code>)</td>
<tr>
<td><code><span class="cfg">C</span> >= <span class="obs">O</span></code></td>
<td>... to a configuration matching with the observation <code><span class="obs">O</span></code> (equiv to <code><span class="cfg">C</span> >= +<span class="obs">O</span></code>)</td>
</tr>
<tr>
<td style="padding: 0px 8px; border-right: 1px solid black;"><code><span style="color:blue">C</span> >= fixed(<span style="color:purple">O</span>)</code></td>
<td style="padding: 0px 8px;">... to a configuration in a trap space where the observation <code><span style="color:purple">O</span></code> is fixed</td>
<td><code><span class="cfg">C</span> >= fixed(<span class="obs">O</span>)</code></td>
<td>... to a configuration in a trap space where the observation <code><span class="obs">O</span></code> is fixed</td>
</tr>
<tr style="background-color: #EEEEEE;">
<td colspan="2" style="padding: 0px 8px; font-style: italic;">Note: can be composed, e.g., <code><span style="color:blue">C1</span> >= <span style="color:blue">C2</span> >= fixed(<span style="color:blue">C3</span>)</code></td>
<tr>
<td colspan="2" style="border: none; font-style: italic;">Note: can be composed, e.g., <code><span class="cfg">C1</span> >= <span class="cfg">C2</span> >= fixed(<span class="cfg">C3</span>)</code></td>
</tr>
<tr>
<td style="padding: 0px 8px; border-right: 1px solid black;"><code><span style="color:blue">C</span> / _</code> or <code>nonreach(<span style="color:blue">C</span>, _)</code></td>
<td style="padding: 0px 8px;">Absence of MP trajectory from the configuration <code><span style="color:blue">C</span></code> to ... (same as reach)</td>
<td><code><span class="cfg">C</span> / _</code> or <code>nonreach(<span class="cfg">C</span>, _)</code></td>
<td style="padding: 0px 8px;">Absence of MP trajectory from the configuration <code><span class="cfg">C</span></code> to ... (same as reach)</td>
</tr>
</table>


#### Universal properties

<table style="margin-left: 0 !important; margin-right: auto !important;">
<table class="language">
<tr>
<td style="padding: 0px 8px; border-right: 1px solid black;"><code>all_fixpoints({<span style="color:purple">O</span>,<span style="color:purple">O'</span>,..})</code></td>
<td style="padding: 0px 8px;">All the fixed points match with at least one given observation</td>
<td><code>all_fixpoints({<span class="obs">O</span>,<span class="obs">O'</span>,..})</code></td>
<td>All the fixed points match with at least one given observation</td>
</tr>
<tr style="background-color: #EEEEEE;">
<td style="padding: 0px 8px; border-right: 1px solid black;">
<code><span style="color:blue">C</span> >> "fixpoints" ^ {<span style="color:purple">O</span>,<span style="color:purple">O'</span>,..}</code></td>
<td style="padding: 0px 8px;">All the fixed points reachable from the configuration <code>C</code> ...</td>
<tr>
<td>
<code><span class="cfg">C</span> >> "fixpoints" ^ {<span class="obs">O</span>,<span class="obs">O'</span>,..}</code></td>
<td>All the fixed points reachable from the configuration <code>C</code> ...</td>
</tr>
</table>


### Contexts

<table style="margin-left: 0 !important; margin-right: auto !important;">
<table class="language">
<tr>
<td style="padding: 0px 8px; border-right: 1px solid black;">
<nobr><code>with mutant({<span style="color:olive">a</span>:0,..} <span style="color:gray">|</span> <span style="color:green">S</span>):</code></nobr><br>
<td>
<nobr><code>with mutant({<span class="bokey">a</span>:0,..} <span style="color:gray">|</span> <span class="some">S</span>):</code></nobr><br>
<code>&nbsp;&nbsp;&nbsp;&nbsp;...</code>
</td>
<td style="padding: 0px 8px;">The properties within the <code>with</code> block are subject to mutation specified by <code>{<span style="color:olive">a</span>:0,..}</code> (resp. <code><span style="color:green">S</span></code>)</td>
<td>The properties within the <code>with</code> block are subject to mutation specified by <code>{<span class="bokey">a</span>:0,..}</code> (resp. <code><span class="some">S</span></code>)</td>
</tr>
</table>
2 changes: 1 addition & 1 deletion theory/most-permissive.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -20,7 +20,7 @@ A subcube $h$ is *smaller* than a subcube $h'$, denoted by $h \preceq h'$ whenev
### Most permissive dynamics

Given a set of components $K\subseteq \{1,\cdots,n\}$, a subcube $h$ is **$K$-closed** by $f$ whenever,
for each component $i\in K$, either $i$ is free in $h$, i.e., $h_i=*$, or $f_i$ applied to any vertices of $h$
for each component $i\in K$ that is fixed in $h$, $f_i$ applied to any vertices of $h$
results in $h_i$. In other words, for all configurations in the $K$-closed subcube $h$,
the next states of the components $i \in K$ are in $h$:
$\forall x\in c(h),\, \forall i\in K,\, h_i\neq *\Rightarrow f_i(x)=h_i$.
Expand Down

0 comments on commit 03c7ef1

Please sign in to comment.