GitLab

commit 99e2fe64 is covered by this improvement.

1 1 Add 0 1 10 ; 2 1 Add 2 2 10 ; 1 2 effect ; 3 2 Rmv 1 ; 4 2 Add 1 2 10 ; 3 1 effect
1 -1 0 null 0,1
[op_table]:
  - rwflinsert list1 null 1 e 10 0 0 0 ; rwflinsert list1 null 1 e 10 0 0 0 1,0,0 0,0|0
  - rwflinsert list1 2 2 e 10 0 0 0 ;
  - rwflrem list1 1 ; rwflrem list1 1 0,1|1
  - rwflinsert list1 1 2 e 10 0 0 0 ; rwflinsert list1 1 2 e 10 0 0 0 2,1,0 0,0|1
[steps]:
  - FULL 0 0
  - FULL 1 0
  - EFFECT 0 1
  - FULL 2 1
  - FULL 3 1
  - EFFECT 2 0
[script state] -- 1 -2 0 null [0,1] ;
[server state] -- 1 -1 10 null [0,1] ;
                  1 -1 10 null [0,1] ; 2 1 10 null [] ;

1 2 Add 0 1 10 ; 2 2 Rmv 1 ; 2 1 effect ; 1 1 effect
1 -1 0 null 0,1

[op_table]:
  - rwflinsert list1266 null 1 e 10 0 0 0 ; rwflinsert list1266 null 1 e 10 0 0 0 1,1,0 0,0|1
  - rwflrem list1266 1 ; rwflrem list1266 1 0,1|1
[steps]:
  - FULL 0 1
  - FULL 1 1
  - EFFECT 1 0
  - EFFECT 0 0
[script state] -- 1 -2 0 null [0,1] ;
[server state] --
                  1 -1 10 null [0,1] ;

- implementation bug could be found by model checking
- final print : add element id

- no random leid optimization for testing mode
- rwflestatusall operation, for read all list element status. (not implemented yet)

No longer need to dump dot graph file, and then use gvpr to parse it.

tlc parameter: -userFile result.txt

test script for rwf-rpq passed

script:
2
1 1 Add 10 ; 2 1 Add 10 ; 3 1 Inc -3 ; 3 2 effect ; 4 2 Add 20 ; 1 2 effect ;
1 10 -3 n ; 1 10 -3 n ;