extend test cases / examples

[pjljvandelaar]

I would like to add Fibonacci as an example or test case.

CHANDEF Channels ::=
    Input, Output :: Int
ENDDEF  

STAUTDEF fibonacci [Input, Output :: Int]() ::=
VAR fibm, fibn, count :: Int
STATE inputState, outputState
INIT inputState{ fibm := 1
               ; fibn := 1
               ; count := -1
               }
TRANS
inputState  -> Input  ? n           [[ (n > 1) /\ (n < 100) ]]     { count := n - 1 }                           -> outputState

outputState -> Output ! fibm + fibn [[ count == 1]] { fibm := 1; fibn := 1; count := -1 }                     -> inputState
outputState -> Output ! fibm + fibn [[ count > 1 ]] { fibm := fibn; fibn := fibm + fibn; count := count - 1 } -> outputState
ENDDEF 

MODELDEF Model ::=
    CHAN IN Input
    CHAN OUT Output

    BEHAVIOUR
    fibonacci [Input, Output]()
ENDDEF 

I prefer to add it as an example, since it also explains what an update list is and how it works (simultaneous assignment of all variables using the old values) This concept was not understood by one of our TorXakis users.

It must be added since I made a change to TxsHappy.y that resulted in no falling tests, yet Fibonacci didn't work....

sqatt-0.1: test (suite: benchmarks-sanity-test)

Choice
  100 choices
Enable
  sequence of enable operators, without data
  sequence of enable operators, with integers
  sequence of enable operators, with integers and two outputs
Hiding
  alternate 4 hide 1 action
  hide first of sync first alternate
...................................................  hide second of sync second
alternate
  match
  match Int
Parallel
  4 parallel sequential-processes
  4 parallel sequential-processes, with internal step
  4 parallel sequential-processes, with alternating actions
  4 parallel sequential-processes, with multiple actions
  convoluted parallel-synchronous model
  4 parallel nested synchronizing sequences
RealWorld
  Multiple Control Loops Stepper
...........  Customers and Orders
  Moving Arms
  Moving Arms (Purpose)
Sequence
  100 actions
  100 internal actions
  100 data actions
  sequence with a 10 integer channel
  sequence with a 10 integer channel (cvc4)
  sequence with a 10 integer channel, using a custom type
Synchronization
  alternate 2 processes
  3 processes
  3 processes with internal action
  6 sequential processes synchronizing in two actions
  many processes synchronizing at the top
  many processes synchronizing in pairs

Finished in 1546.3687 seconds
31 examples, 0 failures

sqatt-0.1: test (suite: examples-test)

Examples.All
  Adder
WARNING: The presence of SMT solvers was not checked.
         First issue #47 needs to be resolved.
See: https://github.com/TorXakis/TorXakis/issues/47
    Basic
    State Automation
    Parallel Adders
    Replay Adder Trace
    Purp1 - 4 goals
    Purp2 - Operand constraints
    Purp3 - Always +2
  Control Loop
    Stepper
    Spec Produce
    Spec Measure
    Spec Correct
.....    Multiple Loops Stepper #long
  Customers and Orders
    Customers & Orders Test
  Dispatch Process
    Process 01
    Process 02
    Process 03
    Process 04
    Process 05
    Process 05a
    Process 06
    Process 06a
    Process 07
    Process 08
    Process 09
    Process 10 - Data
    Process 12 - Unique ID #long
    Process 12 - Unique ID (Wrong)
    Process 12 - Unique ID (Right)
  Echo
    Stepper
    Simulator
  Lucky People
    Examples Purpose Test
    Lucky By Gender Test
    Random Lucky Test
  Moving Arms
    Stepper Test
    Single Axis Purpose Test
    Restricted Axis Purpose Test
  Point
    Stepper Test
    First Quadrant Test Purpose
  ReadWrite Conflict
    Stepper Test
    Stepper Test for Purp Model
    HitAll7 Purpose Test
    Advanced Stepper Test
  Queue
    Stepper Test
    Stepper Test (Lossy)
    SUT Test
  Stimulus-Response
    Stimulus-Response Test 0
    Stimulus-Response Test 1
    Stimulus-Response Test 2
    Stimulus-Response Test 3
    Stimulus-Response Test 4

Finished in 891.3104 seconds
50 examples, 0 failures

sqatt-0.1: test (suite: integration-test)

Any
  Test 0

Finished in 3.1311 seconds
1 example, 0 failures

sqatt-0.1: test (suite: models-test)

Control Loop #model
..................  Stepper 500
......................................  Spec Produce 100
  Spec Measure 100
  Spec Correct 100
..............................................................  Multiple Loops S
tepper 30
Dispatch Process #model
  Process 01
  Process 02
  Process 03
  Process 04
  Process 05
  Process 05a
  Process 06
  Process 06a
  Process 07
  Process 08
  Process 09
  Process 10 - Data
Lucky People #model
  Stepper 200
Moving Arms #model
  Stepper 200
Queue #model
  Stepper Test 200
  Stepper Test (Lossy) 200
ReadWrite Conflict #model
  Stepper 100
.....  Advanced Stepper 100

Finished in 2747.8430 seconds
23 examples, 0 failures

Completed 2 action(s).

[pjljvandelaar]

Or should we also explain how to use irrelevant values to initialize all variable? I.e.

CONSTDEF irrelevant :: Int ::= -1 ENDDEF

CHANDEF Channels ::=
    Input, Output :: Int
ENDDEF  

--State transitions
STAUTDEF fibonacci [Input, Output :: Int]() ::=

VAR fibm, fibn, count :: Int

STATE inputState, outputState

INIT inputState{ fibm := 1
               ; fibn := 1
               ; count := irrelevant
               }
TRANS
inputState  -> Input  ? n           [[ (n > 1) /\ (n < 100) ]] { count := n - 1 }                             -> outputState

outputState -> Output ! fibm + fibn [[ count == 1]] { fibm := 1; fibn := 1; count := irrelevant }             -> inputState
outputState -> Output ! fibm + fibn [[ count > 1 ]] { fibm := fibn; fibn := fibm + fibn; count := count - 1 } -> outputState
ENDDEF 

--System model
MODELDEF Model ::=
    CHAN IN Input
    CHAN OUT Output

    BEHAVIOUR
    fibonacci [Input, Output]()
ENDDEF 

[pjljvandelaar]

Or should we only use the assignment count := irrelevant in the initialization? By leaving it out, we might gain some performance... but loose readability....