[P8-65] Add peterson lcgs

[MathiasMehl]

Adds lcgs implementation of the peterson algorithm. Note that the implemented version is the Filter algorithm, which can be used when there are more than 2 processes (original peterson is limited to 2 processes), see https://en.wikipedia.org/wiki/Peterson%27s_algorithm.

Versions with 2-9 processes are added, in their own directory. In their directory, there can also be found 3 formulae, in both a json and atl version. If you want to look through the implementation of the algorithm, just look in the peterson-02.lcgs, the versions with more processes are similar, just scaled to more processes.

ensure-mutual-exclusion-TRUE-02 tests if no matter what the players choose to do, there will always be at most 1 process in the critical section. ATL version is [[p0,p1]] G (mutual_exclusion). The json version uses despite invariant, which at the moment is buggy and returns wrong result, so perhaps don't look to closely on this one.

multiple-in-CS-FALSE-02 tests if we at any point can reach a state with more than one process in the critical section. Very similar to above, but uses enforce eventually instead in the json version, returns correct result. ATL version <<p0,p1>> F (multiple_in_cs).

p0-eventually-reach-CS-TRUE-02 tests if the process p0 can eventually reach the critical section. ATL version <<p0,p1>> F (p0_in_cs).

The labels used in the ATL versions can be seen first in the peterson-0*.lcgs

Right now it introduces ALOT of files, this can be reduced by fixing issue #104 so there wont be many very alike files.

[NicEastvillage]

PR #99 has been merged into main. Please merge main into your branch and move the Peterson LCGS to the lcgs-examples folder.

[lars4509]

Looks good to me.
While this problem is interesting, it might not be as interesting in the ATL perspective, since all formulas are affecting all players and in that case could be expressed with CTL (correct me if i am wrong). That said it still might suit as a good test case.