Generalized choice about torxakis HOT 7 CLOSED

Thanks for the examples! Let me check my understanding:

1. Supports a finite range of random values, the tester searches for a process within this range that accepts the SUT.
2. Defines the model from a tester's perspective, modelling the clients' knowledge of the SUT.
3. Test is specified as a channel provided by SUT. Servers not sending data to Test violate the model.

If so, that solves my question!

from torxakis.

Looking at your example code, have you considered
Data ? x [[(0 <= x) /\ (x <= 12345)]]
or even just Data ? x?

from torxakis.

Passes parser but doesn't step:

PROCDEF rand [Data :: Int] () ::=
        Data ? x -- with or without [[(0 <= x) /\ (x <= 12345)]]
ENDDEF

TXS >> input files parsed:
TXS >> ["q.txs"]
TXS >> stepper Model
TXS >> unfoldCTbranch: Not unique
TXS >> Stepper started
TXS >> stepper 10
TXS >> NoOp : No action

The ## approach could step.

from torxakis.

Another attempt:

PROCDEF rand [Data :: Int] (x :: Int) ::=
        Data ! x
     ## rand [Data] (x + 1)
ENDDEF

stepper Model does not return, process txsserver is busy.

from torxakis.

The another attempt is an infinite model: causing, as observed, an infinite unfolding in txsserver.

from torxakis.

Torxakis assumes (for efficient calculation/limits of problem solvers) that the value communicated over hidden channels must be uniquely solvable. Your model violates this assumption.
When I have access to a pc, I will add a model that does what you want when the range of values is limited, which seems to be the case in your example where the range is from 0 up to 9.

from torxakis.

Today at the lab, so I could also access the article ;-)

TorXakis does not support generalized choice as specified by the Lotos paper.
TorXakis support however at least three alternatives:

1. using dynamic process creation

PROCDEF q [In :: Int; Out :: Bool] (data :: Int) ::=
        In  ? request
    >-> Out ! request == data
    >-> q [In, Out] (data)
ENDDEF

PROCDEF qs [In :: Int; Out :: Bool] (nr :: Int) ::=
        q [In,Out] (nr)
    ## 
        [[nr >= 0]] =>> qs[In,Out] (nr-1)
ENDDEF

PROCDEF server [In :: Int; Out :: Bool] () ::=
    qs[In,Out](9)
ENDDEF

See for the whole file issue952.alt1.txt
Note: that LPE and LpeOps don't support dynamic process creation.

2. Using a list of different numbers
   When request == data is False we don't learn the value of data, we only learn a value that is different to data.

PROCDEF q [In :: Int; Out :: Bool] (data :: Int) ::=
        In  ? request
    >-> Out ! request == data
    >-> q [In, Out] (data)
ENDDEF

TYPEDEF List ::= Nil | Cstr { head :: Int; tail :: List } ENDDEF

FUNCDEF in ( i :: Int; l :: List ) :: Bool ::= 
IF isNil (l) THEN False 
             ELSE IF head (l) == i THEN True 
                                   ELSE in (i, tail(l))
                  FI
FI 
ENDDEF

PROCDEF unknown [In :: Int; Out :: Bool] (ds :: List) ::=
        In  ? request
    >-> (  [[ in (request, ds) ]] =>> Out ! False >-> unknown [In, Out] (ds)
        ## [[not (in (request, ds)) ]] =>> (  Out ! True >-> q [In, Out](request)
                                           ## Out ! False >-> unknown [In, Out] (Cstr(request, ds))
                                           )
        )
ENDDEF

PROCDEF server [In :: Int; Out :: Bool] () ::=
    unknown[In,Out](Nil)
ENDDEF

See for the whole file issue952.alt2.txt

3. Using a test interface

PROCDEF q [In :: Int; Out :: Bool] (data :: Int) ::=
        In  ? request
    >-> Out ! request == data
    >-> q [In, Out] (data)
ENDDEF

PROCDEF server [In :: Int; Test :: Int; Out :: Bool] () ::=
  Test ? data >-> q [In, Out](data)
ENDDEF

CHANDEF ChanDefs ::=
   In  :: Int;
   Out :: Bool;
   Test :: Int
ENDDEF

MODELDEF Model ::=
  CHAN IN  In
  CHAN OUT Out, Test

  BEHAVIOUR server [In, Test, Out] ()
ENDDEF

For the whole file see issue952.alt3.txt

I hope this helps!
If so you can close the issue.

from torxakis.