Re: [tlaplus] How to model database tables?

[Stephan Merz <stepha...@xxxxxxxxx>]

Hello,

your spec of a simple data base looks good to me. Two minor comments:

. The conjunct "defectTypes[id] /= data" in action Update ensures that the action is different from a stuttering action. Whether you leave it in or not is unobservable and doesn't make a difference to the properties of your spec since TLA+ always allows for stuttering transitions (and if there were a fairness requirement on Update actions, it would only constrain non-stuttering updates). The two actions Add and Update could perhaps even be merged – but that would make a difference due to the fairness condition that requires Add actions (but not Update actions) to occur.

. In the fairness condition, requiring weak or strong fairness doesn't make a difference since the action is enabled as long as there exists some item with entry "Nope", and that condition can become false only by the action occurring. Also, the condition is stronger than what the informal description says: it requires that whenever there exists some item for which the entry is "Nope", some defect will eventually be added to the data base. It is non-trivial to write a fairness condition that expresses that it's enough for only one Add action to occur over the lifetime of the system. You'd probably have to add a variable, say, defectAdded, that remembers if some Add action occurred: initialize the variable to FALSE and set it to TRUE during an Add (irrespective of its old value), then require 

  WF_vars(\E id \in TYPEID, data \in DATA : ~defectAdded /\ Add(id, data))

One way to observe the difference is by verifying the property

  []<>(\E id \in TYPEID : defectTypes[id] \in Data)

which will be true for your current spec but false for the one for the weaker fairness condition, since it's enough for an item to be added at some point, but this entry can be deleted later on. That is, the weaker spec only satisfies

  <>(\E id \in TYPEID : defectTypes[id] \in Data).

Regards,
Stephan


> On 29 Dec 2017, at 11:22, Justin Scott <justin.ja...@xxxxxxxxx> wrote:
> 
> Hi all. Played on and off with TLA+ over the years but really got a recent knowledge boost from the video series (thanks, Leslie).
> 
> I've decided to take an unfinished home project of making a PSP (personal software process) database system and model it in TLA+. In a nutshell, the system is:
> 	• Time log.
> 	• Defect log.
> 	• A process (what steps to do when).
> 	• A project that follows the steps of a process.
> The interesting (and undiscovered) part of the design is this:
> 
> 	• How should the system behave when you're partway through a project and then the process changes that is guiding the project?
> Before I go too far down the wrong path, can someone tell me if my approach to modeling a single database table is correct (in this case a table of defect types)?
> 
> 
> 
> I chose to do a function from an "id" (say the primary key of a SQL table) to a "data" (the rest of the columns of a SQL table) or a constant indicating no row was found.
> 
> 
> 
> Hope you all had a great holidays. :)
> 
> 
> -- 
> You received this message because you are subscribed to the Google Groups "tlaplus" group.
> To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+u...@xxxxxxxxxxxxxxxx.
> To post to this group, send email to tla...@xxxxxxxxxxxxxxxx.
> Visit this group at https://groups.google.com/group/tlaplus.
> For more options, visit https://groups.google.com/d/optout.
> <DefectType.tla>