View source for PKC Workflow/System Verification by TLA+/Process/Planning



== Planning == 
As TLA+ is well-suited to model and verify a system, I think it has differences from other monitoring tools.  These tools analyze the operational data(dynamic)  to decide whether the system reach the desired status, while TLA+ analyzes the specification (static) before a system is running.  To integrate with PKC, the [[Success Criteria]] is a good start as it can contain [[Criteria:Safety]] and [[Criteria:Liveness]] conditions.  After we specified [[Success Criteria]], we start designing the [[Process]].  The TLA+ can then verify the design after the process is specified.  In order to bridge the success conditions with the design, we should describe the design from a proper perspective.  After that, the code could be abstracted into states and states transformations.  We can then use the [https://lamport.azurewebsites.net/tla/tools.html TLC model checker] to get the analysis of the specification.  



== [[Book/Specifying Systems]] Notes == 
<blockquote> 
<p>
A specification is a mathematical model of a particular view of some part of a system. When writing a specification, the first thing you must choose is exactly what part of the system you want to model. 
</p> 
</blockquote>

<blockquote> 
<p>
It can be used to write a precise, formal description of almost any sort of discrete system. It’s especially well suited to describing asynchronous systems—that is, systems with components that do not operate in strict lock-step. 
</p> 
</blockquote>

== List of current TLA+ examples == 
* [https://www.hillelwayne.com/list-of-tla-examples/ List of TLA examples]
== Producer-Consumer example [https://www.cs.unh.edu/~charpov/programming-tlabuffer.html]== 
Take an example to show how success criteria bridge the code.  

{{LogicModel|name=Producer-Consumer System}}





<syntaxhighlight> 
EXTENDS Naturals, Sequences

CONSTANTS Producers,   (* the (nonempty) set of producers                           *)
          Consumers,   (* the (nonempty) set of consumers                           *)
          BufCapacity, (* the maximum number of messages in the bounded buffer      *)
          Data         (* the set of values that can be produced and/or consumed    *)

ASSUME /\ Producers # {}                      (* at least one producer *)
       /\ Consumers # {}                      (* at least one consumer *)
       /\ Producers \intersect Consumers = {} (* no thread is both consumer and producer *)
       /\ BufCapacity > 0                     (* buffer capacity is at least 1 *)
       /\ Data # {}                           (* the type of data is nonenpty *) 
...
</syntaxhighlight>

== Meta == 
* Links are crucial to fill in the information and optimize a paragraph's structure 
* It could be useful to automatically recognize the information entity behind the natural language.
* The quote of a pdf could be structured using annotation tools
* [Decision point]: When naming Producer-Consumer System, it is difficult to decide whether to add the prefix of ''TLA Workflow/Process/Planning''.  If we do, then the page will be hidden in the hierarchy (though it could be solved by [[ignoring the hierarchical structure]]); if not, the page is lift up to the top with the context eliminated so we might need to add the context back in the logic model.  In [[Relate with::Namespace Management]] , it might be the correct way to think whether the page contains the context.
* The [[intention primitive]]

== Discussion == 
* We can see that software and content becoming more indistinguishable as more content could be structured or formalized.  For example, the [[Book/Provisional_Patent_Application#3.2/Conceptual Modules]] use fuzzy logic to translate each piece of opinion into a string of alpha-numeric text.
* In AI field, researchers try to find the "right representation" which enable the machine to understand knowledge and perform more advanced knowledge task such as reasoning.  The Logic model that we work on is currently not intended to express all the knowledge.  Instead, it aims to provide a high-level abstraction of knowledge which helps the search for domain specific language.
* Once a domain-specific language structures a domain well, then the domain is computable.
* The strength of TLA+ is to enumerate all the states of a temporal system. 
* A knowledge engine could do inferencing and reasoning over knowledge.  The corresponding language, such as rewrite system, type system, etc, will also be integrated in the future.