Stephan, thanks for taking a look.
I can see what you're saying about the stuttering step. That was very helpful.
I had originally considered making Add and Update the same action. Often in my work with SQL I write the code that way as well. I guess I was resisting the "pull" of TLA+ to reduce itself to something more minimal. Even the first AddUpdate would need to be an add in order to be a non-stuttering step.
I think perhaps the fairness is not appropriate for this part of the system. This spec is really about categories of defects rather than defects themselves. The thought was that in setting up a project, you'd want to know how to classify bugs. However, there is not guarantee that you'll have a bug in a project (hehe... haha... hoho... at least theoretically). So it may be better represented by just describing the action for adding bugs requiring a bug type to exist. If there were no need to add a bug there would be no need for a bug type to exist.
Although I modeled the fairness wrong, I appreciate your insights on it: creating a condition that can be passed by SF and failed by WF in order to tease out the nuances between the two. Thanks.
On Friday, December 29, 2017 at 2:22:40 AM UTC-8, Justin Scott 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. :)