Fork, Commit, Merge - Easy Issue (TLA+)

[nikohoffren]

Fork, Commit, Merge - Easy Issue (TLA+)

Specify a Simple Counter

Note: You don't have ask permission to start solving the issue or get assigned, since these issues are supposed to be always open for new contributors. The actions-user bot will reset the file back to previous state for the next contributor after your commit is merged. So you can just simply start working with the issue right away!

Objective:

Your task is to design a TLA+ specification for a simple counter. The counter should start at 0 and have the ability to increment and decrement, but it should never go below 0.

Acceptance Criteria:

• The counter must start at 0.
• The counter can be incremented.
• The counter can be decremented, but never go below 0.

How to get started:

You can create the counter inside VS Code.
Open up the counter.tla file inside of tasks/tla+/easy directory and start implementing your solution!

How to test the solution

• Open up the TLA+ Toolbox program, that you should have installed.
• Create a new spec by selecting File > New Spec.
• Navigate to and select the .tla file you wrote in VS Code.
• Once the specification is loaded, create a new model by clicking the TLC Model Checker > New Model.
  You can use the default name for the model and just click OK.
• Click the TLC Model Checker again and open up the TLC Console so you can see the output.
• Start running the model checking process by clicking TLC Model Checker > Run Model or just simply press F11.
  This will run the check and you will see the output in the console.

You should see something like this:

Starting... (2023-08-18 10:28:04)
Computing initial states...
Finished computing initial states: 1 distinct state generated at 2023-08-18 10:28:05.
Model checking completed. No error has been found.
  Estimates of the probability that TLC did not check all reachable states
  because two distinct states had the same fingerprint:
  calculated (optimistic):  val = 5.5E-16
The coverage statistics at 2023-08-18 10:28:05
<Init line 9, col 1 to line 9, col 4 of module counter>: 1:1
  line 9, col 9 to line 9, col 17 of module counter: 1
<Increment line 11, col 1 to line 11, col 9 of module counter>: 100:100
  line 12, col 6 to line 12, col 21 of module counter: 100
  |line 12, col 6 to line 12, col 10 of module counter: 101
  |line 12, col 14 to line 12, col 21 of module counter: 101
  line 13, col 6 to line 13, col 23 of module counter: 100
<Decrement line 15, col 1 to line 15, col 9 of module counter>: 0:100
  line 16, col 6 to line 16, col 14 of module counter: 100
  |line 16, col 6 to line 16, col 10 of module counter: 101
  line 17, col 6 to line 17, col 23 of module counter: 100
End of statistics.
Progress(101) at 2023-08-18 10:28:05: 201 states generated (12,381 s/min), 101 distinct states found (6,221 ds/min), 0 states left on queue.
201 states generated, 101 distinct states found, 0 states left on queue.
The depth of the complete state graph search is 101.
The average outdegree of the complete state graph is 1 (minimum is 0, the maximum 1 and the 95th percentile is 1).
Finished in 981ms at (2023-08-18 10:28:05)

Main thing is that there are no errors to be found. If your output looks like all of the operators are working just fine, you are ready to make a pull request!

---

To work with this issue, you need to have TLA+ Toolbox installed to your local machine.
Check out README.md for more instructions of installing TLA+ Toolbox and how to make a pull request.

Feel free to ask any questions here if you have some problems!

Also, kindly give this project a star to enhance its visibility for new developers!