Skip to content

Commit

Permalink
Update
Browse files Browse the repository at this point in the history
  • Loading branch information
@penglei
penglei committed Feb 2, 2022
1 parent 595e718 commit 5a7b409
Show file tree
Hide file tree
Showing 37 changed files with 326 additions and 170 deletions.
2 changes: 1 addition & 1 deletion 404.html
View file
Original file line number Diff line number Diff line change
Expand Up @@ -161,7 +161,7 @@ <h1 class="error-emoji"></h1>
<span class="copyright-year">
&copy;
2017 -
2021
2022
<span class="heart">
<i class="iconfont icon-heart"></i>
</span>
Expand Down
3 changes: 2 additions & 1 deletion about/index.html
View file
Original file line number Diff line number Diff line change
Expand Up @@ -164,6 +164,7 @@
\newcommand{\PICK}{\sc{PICK}}
\newcommand{\WITNESS}{\sc{WITNESS}}
\newcommand{\HIDE}{\sc{HIDE}}
\newcommand{\@w}[1]{\textsf{``{#1}''}}
</script>
</div>

Expand Down Expand Up @@ -254,7 +255,7 @@
<span class="copyright-year">
&copy;
2017 -
2021
2022
<span class="heart">
<i class="iconfont icon-heart"></i>
</span>
Expand Down
4 changes: 2 additions & 2 deletions categories/formal/index.html
View file
Original file line number Diff line number Diff line change
Expand Up @@ -142,7 +142,7 @@ <h2 class="archive-name">Formal</h2>
</span>
<span class="archive-post-title">
<a href="/post/specifying-systems-notes-2/" class="archive-post-link">
Specifying Systems 笔记2 Liveness &amp; Fairness
Specifying Systems 笔记2 Liveness
</a>
</span>
</div>
Expand Down Expand Up @@ -179,7 +179,7 @@ <h2 class="archive-name">Formal</h2>
<span class="copyright-year">
&copy;
2017 -
2021
2022
<span class="heart">
<i class="iconfont icon-heart"></i>
</span>
Expand Down
10 changes: 5 additions & 5 deletions categories/formal/index.xml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -12,20 +12,20 @@


<item>
<title>Specifying Systems 笔记2 Liveness &amp; Fairness</title>
<title>Specifying Systems 笔记2 Liveness</title>
<link>/post/specifying-systems-notes-2/</link>
<pubDate>Tue, 08 Sep 2020 21:00:00 +0800</pubDate>

<guid>/post/specifying-systems-notes-2/</guid>
<description>&lt;div id=&#34;preamble&#34;&gt;
&lt;div class=&#34;sectionbody&#34;&gt;
&lt;div class=&#34;paragraph&#34;&gt;
&lt;p&gt;Specifying Systems的1-7章层层推进，在实例中穿插着原理讲解，深入浅出地讲解了Specification是什么，以及如何规约系统设计。
&lt;p&gt;Specifying Systems的1-7章层层推进，在实例中穿插着原理讲解，深入浅出地讲解了Specification是什么，以及如何设计系统规约。
这些Specification表明了系统的Safety属性&amp;#8201;&amp;#8212;&amp;#8201;即系统行为被约束在一定范围内，不会做出一些不被允许的行为(something &lt;strong&gt;bad&lt;/strong&gt; does not happen)。
在TLA+中，通常使用公式 \(Spec \triangleq Init \land \Box [Next]_{vars}\) 来描述系统的Safety属性(约束)。
Safety属性说明了系统中什么不能发生，但无法表达系统中&lt;strong&gt;最终会发生&lt;/strong&gt;的这类属性，而Liveness便可以表达(&#34;something &lt;strong&gt;good&lt;/strong&gt; eventully happen&#34;)。
Liveness使用时态逻辑公式进行描述，一个系统规约可以通过公式 \(Spec \triangleq Init \land \Box [Next]_{vars} \land F\) 来同时描述其对Safety和Liveness的要求，
公式末尾的 $F$ 便是描述Liveness属性的公式。&lt;/p&gt;
Safety属性说明了系统中什么不能发生，但无法表达系统中&lt;strong&gt;某些时间一定会发生&lt;/strong&gt;的这类属性，而Liveness便可以表达(&#34;something &lt;strong&gt;good&lt;/strong&gt; eventully happen&#34;)。
Liveness使用时态逻辑公式进行描述，一个系统规约可以通过公式 \(Spec \triangleq Init \land \Box [Next]_{vars} \land L\) 来同时描述其对Safety和Liveness的要求，
公式末尾的 $L$ 便是描述Liveness属性的公式。&lt;/p&gt;
&lt;/div&gt;&lt;/div&gt;&lt;/div&gt;</description>
</item>

Expand Down
2 changes: 1 addition & 1 deletion categories/homelab/index.html
View file
Original file line number Diff line number Diff line change
Expand Up @@ -170,7 +170,7 @@ <h2 class="archive-name">homelab</h2>
<span class="copyright-year">
&copy;
2017 -
2021
2022
<span class="heart">
<i class="iconfont icon-heart"></i>
</span>
Expand Down
2 changes: 1 addition & 1 deletion categories/index.html
View file
Original file line number Diff line number Diff line change
Expand Up @@ -176,7 +176,7 @@
<span class="copyright-year">
&copy;
2017 -
2021
2022
<span class="heart">
<i class="iconfont icon-heart"></i>
</span>
Expand Down
2 changes: 1 addition & 1 deletion categories/network/index.html
View file
Original file line number Diff line number Diff line change
Expand Up @@ -179,7 +179,7 @@ <h2 class="archive-name">network</h2>
<span class="copyright-year">
&copy;
2017 -
2021
2022
<span class="heart">
<i class="iconfont icon-heart"></i>
</span>
Expand Down
2 changes: 1 addition & 1 deletion categories/proxy/index.html
View file
Original file line number Diff line number Diff line change
Expand Up @@ -170,7 +170,7 @@ <h2 class="archive-name">proxy</h2>
<span class="copyright-year">
&copy;
2017 -
2021
2022
<span class="heart">
<i class="iconfont icon-heart"></i>
</span>
Expand Down
2 changes: 1 addition & 1 deletion categories/servicemsh/index.html
View file
Original file line number Diff line number Diff line change
Expand Up @@ -170,7 +170,7 @@ <h2 class="archive-name">servicemsh</h2>
<span class="copyright-year">
&copy;
2017 -
2021
2022
<span class="heart">
<i class="iconfont icon-heart"></i>
</span>
Expand Down
12 changes: 6 additions & 6 deletions index.html
View file
Original file line number Diff line number Diff line change
Expand Up @@ -125,7 +125,7 @@
<section id="posts" class="posts">
<article class="post">
<header class="post-header">
<h1 class="post-title"><a class="post-link" href="/post/specifying-systems-notes-2/">Specifying Systems 笔记2 Liveness &amp; Fairness</a></h1>
<h1 class="post-title"><a class="post-link" href="/post/specifying-systems-notes-2/">Specifying Systems 笔记2 Liveness</a></h1>
<div class="post-meta">
<span class="post-time"> 2020-09-08 </span>
<div class="post-category">
Expand All @@ -139,12 +139,12 @@ <h1 class="post-title"><a class="post-link" href="/post/specifying-systems-notes
<div id="preamble">
<div class="sectionbody">
<div class="paragraph">
<p>Specifying Systems的1-7章层层推进，在实例中穿插着原理讲解，深入浅出地讲解了Specification是什么，以及如何规约系统设计。
<p>Specifying Systems的1-7章层层推进，在实例中穿插着原理讲解，深入浅出地讲解了Specification是什么，以及如何设计系统规约。
这些Specification表明了系统的Safety属性&#8201;&#8212;&#8201;即系统行为被约束在一定范围内，不会做出一些不被允许的行为(something <strong>bad</strong> does not happen)。
在TLA+中，通常使用公式 \(Spec \triangleq Init \land \Box [Next]_{vars}\) 来描述系统的Safety属性(约束)。
Safety属性说明了系统中什么不能发生，但无法表达系统中<strong>最终会发生</strong>的这类属性，而Liveness便可以表达("something <strong>good</strong> eventully happen")。
Liveness使用时态逻辑公式进行描述，一个系统规约可以通过公式 \(Spec \triangleq Init \land \Box [Next]_{vars} \land F\) 来同时描述其对Safety和Liveness的要求，
公式末尾的 $F$ 便是描述Liveness属性的公式。</p>
Safety属性说明了系统中什么不能发生，但无法表达系统中<strong>某些时间一定会发生</strong>的这类属性，而Liveness便可以表达("something <strong>good</strong> eventully happen")。
Liveness使用时态逻辑公式进行描述，一个系统规约可以通过公式 \(Spec \triangleq Init \land \Box [Next]_{vars} \land L\) 来同时描述其对Safety和Liveness的要求，
公式末尾的 $L$ 便是描述Liveness属性的公式。</p>
</div></div></div>
</div>
<div class="read-more">
Expand Down Expand Up @@ -345,7 +345,7 @@ <h1 class="post-title"><a class="post-link" href="/post/asciidoc-preview/">Ascii
<span class="copyright-year">
&copy;
2017 -
2021
2022
<span class="heart">
<i class="iconfont icon-heart"></i>
</span>
Expand Down
10 changes: 5 additions & 5 deletions index.xml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -22,20 +22,20 @@
</item>

<item>
<title>Specifying Systems 笔记2 Liveness &amp; Fairness</title>
<title>Specifying Systems 笔记2 Liveness</title>
<link>/post/specifying-systems-notes-2/</link>
<pubDate>Tue, 08 Sep 2020 21:00:00 +0800</pubDate>

<guid>/post/specifying-systems-notes-2/</guid>
<description>&lt;div id=&#34;preamble&#34;&gt;
&lt;div class=&#34;sectionbody&#34;&gt;
&lt;div class=&#34;paragraph&#34;&gt;
&lt;p&gt;Specifying Systems的1-7章层层推进，在实例中穿插着原理讲解，深入浅出地讲解了Specification是什么，以及如何规约系统设计。
&lt;p&gt;Specifying Systems的1-7章层层推进，在实例中穿插着原理讲解，深入浅出地讲解了Specification是什么，以及如何设计系统规约。
这些Specification表明了系统的Safety属性&amp;#8201;&amp;#8212;&amp;#8201;即系统行为被约束在一定范围内，不会做出一些不被允许的行为(something &lt;strong&gt;bad&lt;/strong&gt; does not happen)。
在TLA+中，通常使用公式 \(Spec \triangleq Init \land \Box [Next]_{vars}\) 来描述系统的Safety属性(约束)。
Safety属性说明了系统中什么不能发生，但无法表达系统中&lt;strong&gt;最终会发生&lt;/strong&gt;的这类属性，而Liveness便可以表达(&#34;something &lt;strong&gt;good&lt;/strong&gt; eventully happen&#34;)。
Liveness使用时态逻辑公式进行描述，一个系统规约可以通过公式 \(Spec \triangleq Init \land \Box [Next]_{vars} \land F\) 来同时描述其对Safety和Liveness的要求，
公式末尾的 $F$ 便是描述Liveness属性的公式。&lt;/p&gt;
Safety属性说明了系统中什么不能发生，但无法表达系统中&lt;strong&gt;某些时间一定会发生&lt;/strong&gt;的这类属性，而Liveness便可以表达(&#34;something &lt;strong&gt;good&lt;/strong&gt; eventully happen&#34;)。
Liveness使用时态逻辑公式进行描述，一个系统规约可以通过公式 \(Spec \triangleq Init \land \Box [Next]_{vars} \land L\) 来同时描述其对Safety和Liveness的要求，
公式末尾的 $L$ 便是描述Liveness属性的公式。&lt;/p&gt;
&lt;/div&gt;&lt;/div&gt;&lt;/div&gt;</description>
</item>

Expand Down
3 changes: 2 additions & 1 deletion post/adding-new-equipment-r630-to-my-homelab/index.html
View file
Original file line number Diff line number Diff line change
Expand Up @@ -182,6 +182,7 @@
\newcommand{\PICK}{\sc{PICK}}
\newcommand{\WITNESS}{\sc{WITNESS}}
\newcommand{\HIDE}{\sc{HIDE}}
\newcommand{\@w}[1]{\textsf{``{#1}''}}
</script>
</div>

Expand Down Expand Up @@ -514,7 +515,7 @@ <h2 id="_测试带宽"><a class="anchor" href="#_测试带宽"></a><a class="lin
<span class="copyright-year">
&copy;
2017 -
2021
2022
<span class="heart">
<i class="iconfont icon-heart"></i>
</span>
Expand Down
Loading

0 comments on commit 5a7b409

Please sign in to comment.