Parsing of SUT messages can result in a MultipleDefinitions error

[brampetersen]

Hi,

TorXakis seems to behave weird when a type only has a single string argument when using the tester. The stepper works fine but when I use the tester it returns the "hGetLine: end of file" error. In the tester I use the following Python string encode (works fine for every other message format): connection.sendall(str.encode('M(\"Up command\")\n'))

Model:

TYPEDEF ITypes0 ::=
	M { v :: String }
ENDDEF

TYPEDEF OTypes0 ::=
	M { v :: String }
ENDDEF

STAUTDEF m0 [ InSut0 :: ITypes0; OutSut0 :: OTypes0; ] ( ) EXIT ::=
	STATE	s0, s1, s2
	VAR  	vi0 :: Int
	INIT 	s0 { vi0 := 0 }
	TRANS	s0 -> InSut0 ?x [[ x == M("Up pressed") ]] -> s1
			s1 -> OutSut0 ?x [[ x == M("Up command") ]] -> s2
			s2 -> EXIT -> s2
ENDDEF

PROCDEF overarching_proc  [ InSut0 :: ITypes0; OutSut0 :: OTypes0; ] ( ) ::=
	(
		m0 [ InSut0, OutSut0 ] ( )
	) >>> overarching_proc [ InSut0, OutSut0 ] ( )
ENDDEF

CHANDEF ChanDefs ::=
	InSut0	::	ITypes0;
	OutSut0	::	OTypes0;
ENDDEF

MODELDEF Model ::=
	CHAN IN 	InSut0
	CHAN OUT	OutSut0

	BEHAVIOUR	overarching_proc [ InSut0, OutSut0 ] ( )
ENDDEF

CNECTDEF Sut ::=
	CLIENTSOCK

	CHAN OUT	InSut0	HOST "localhost" PORT 9990
	ENCODE		InSut0	?x -> !toString(x)
	CHAN IN 	OutSut0	HOST "localhost" PORT 9990
	DECODE		OutSut0	!fromString(x) <- ?x
ENDDEF

Output torxakis:

torxakis 9991 temp.txs        

TXS >>  TorXakis :: Model-Based Testing

TXS >>  txsserver starting: "localhost" : 9991
TXS >>  Solver "z3" initialized : Z3 [4.8.5]
TXS >>  TxsCore initialized
TXS >>  input files parsed:
TXS >>  ["temp.txs"]
TXS >> tester Model Sut
TXS >>  Tester started
TXS >> test 10
TXS >>  .....1: IN: Act { { ( InSut0, [ M("Up pressed") ] ) } }
torxakis: <socket: 31>: hGetLine: end of file

Output txsserver:

txsserver --smt-solver z3 9991
No configuration file found.

TXSSERVER >>  Starting  ..... 

TXSSERVER CMD >>  START
TXSSERVER RSP <<  MACK txsserver starting:  "localhost" : 9991
TXSSERVER RSP <<  PACK START
TXSSERVER CMD >>  INIT ["temp.txs"]
TXSSERVER RSP <<  MACK Solver "z3" initialized : Z3 [4.8.5]
TXSSERVER RSP <<  MACK TxsCore initialized
TXSSERVER RSP <<  MACK input files parsed:
TXSSERVER RSP <<  MACK ["temp.txs"]
TXSSERVER RSP <<  PACK INIT
TXSSERVER CMD >>  TESTER Model Sut
TXSSERVER RSP <<  MACK Tester started
TXSSERVER RSP <<  PACK TESTER
TXSSERVER CMD >>  TEST 10
TXSSERVER RSP <<  MACK .....1:  IN:  Act    { { ( InSut0, [ M("Up pressed") ] ) } }
txsserver: Decode: eval failed
  eval: ASF
vexpr: "M(\"Up command\")"
signatures: Sigs {chan = [ChanId {name = "InSut0", unid = 1092, chansorts = [SortId {name = "ITypes0", unid = 1000}]},ChanId {name = "OutSut0", unid = 1093, chansorts = [SortId {name = "OTypes0", unid = 1001}]}], func = ["%","*","+","++","-","/","/\\","<","<=","<=>","<>","==","=>",">",">=","M","\\/","\\|/","abs","at","dropWhile","dropWhileNot","fromString","fromXml","isM","len","not","strinre","takeWhile","takeWhileNot","toString","toXml","v"], pro = [ProcId {name = "m0", unid = 1077, procchans = [ChanSort [SortId {name = "ITypes0", unid = 1000}],ChanSort [SortId {name = "OTypes0", unid = 1001}]], procvars = [], procexit = Exit []},ProcId {name = "overarching_proc", unid = 1074, procchans = [ChanSort [SortId {name = "ITypes0", unid = 1000}],ChanSort [SortId {name = "OTypes0", unid = 1001}]], procvars = [], procexit = NoExit},ProcId {name = "std_m0", unid = 1078, procchans = [ChanSort [SortId {name = "ITypes0", unid = 1000}],ChanSort [SortId {name = "OTypes0", unid = 1001}]], procvars = [SortId {name = "Int", unid = 102},SortId {name = "Int", unid = 102}], procexit = Exit []},ProcId {name = "stdi_m0", unid = 1079, procchans = [ChanSort [SortId {name = "ITypes0", unid = 1000}],ChanSort [SortId {name = "OTypes0", unid = 1001}]], procvars = [], procexit = Exit []}], sort = fromList [("Bool",SortId {name = "Bool", unid = 101}),("ITypes0",SortId {name = "ITypes0", unid = 1000}),("Int",SortId {name = "Int", unid = 102}),("OTypes0",SortId {name = "OTypes0", unid = 1001}),("Regex",SortId {name = "Regex", unid = 105}),("String",SortId {name = "String", unid = 104})]}
error: MultipleDefinitions Entity at <no location>: Found multiple elements: [SortId {name = "OTypes0", unid = 1001},SortId {name = "ITypes0", unid = 1000}]
CallStack (from HasCallStack):
  error, called at src/TorXakis/Compiler.hs:175:25 in txs-compiler-0.1.0.0-NeT1WHE4z77rZeP6s63kU:TorXakis.Compiler
CallStack (from HasCallStack):
  error, called at src/EnDecode.hs:104:31 in cnect-0.1.7.0-4GkigeKnNQqC7Mf8OnKIF7:EnDecode

The strange thing is, if an argument is added, like:

TYPEDEF OTypes0 ::=
	M { v :: String; i :: Int }
ENDDEF

Then change:

s1 -> OutSut0 ?x [[ x == M("Up command", 1) ]] -> s2

and: connection.sendall(str.encode('M(\"Up command\", 1)\n'))

It works fine:

test 10
TXS >>  .....1: IN: Act { { ( InSut0, [ M("Up pressed") ] ) } }
TXS >>  .....2: OUT: Act { { ( OutSut0, [ M("Up command",1) ] ) } }
TXS >>  .....3: IN: Act { { ( InSut0, [ M("Up pressed") ] ) } }
TXS >>  .....4: OUT: Act { { ( OutSut0, [ M("Up command",1) ] ) } }
TXS >>  .....5: IN: Act { { ( InSut0, [ M("Up pressed") ] ) } }
TXS >>  .....6: OUT: Act { { ( OutSut0, [ M("Up command",1) ] ) } }
TXS >>  .....7: IN: Act { { ( InSut0, [ M("Up pressed") ] ) } }
TXS >>  .....8: OUT: Act { { ( OutSut0, [ M("Up command",1) ] ) } }
TXS >>  .....9: IN: Act { { ( InSut0, [ M("Up pressed") ] ) } }
TXS >>  ....10: OUT: Act { { ( OutSut0, [ M("Up command",1) ] ) } }
TXS >>  PASS

[pjljvandelaar]

A quick analysis shows that the problem is that transforming the string M("Up command") to torxakis is ambiguous.
The ambiguity is caused by:

TYPEDEF ITypes0 ::=
	M { v :: String }
ENDDEF

TYPEDEF OTypes0 ::=
	M { v :: String }
ENDDEF

I.e. two data types have the same constructor (name and argument).

imho TorXakis should be able to distinguish these two data types, since only OType is expected.

[brampetersen]

Thanks for the quick answer. Changing the typedef works:

TYPEDEF OTypes0 ::=
	E { v :: String }
ENDDEF

TXS >> test 1000
TXS >>  .....1: IN: Act { { ( InSut0, [ M("Up pressed") ] ) } }
TXS >>  .....2: OUT: Act { { ( OutSut0, [ E("Up command") ] ) } }
TXS >>  .....3: IN: Act { { ( InSut0, [ M("Up pressed") ] ) } }
TXS >>  .....4: OUT: Act { { ( OutSut0, [ E("Up command") ] ) } }
TXS >>  .....5: IN: Act { { ( InSut0, [ M("Up pressed") ] ) } }

What should I do with the issue, close it?

[pjljvandelaar]

The function compileValExpr lacks a parameter to specify the expected type (when known).
This would disambiguate the value of the string and prevent the reported error.

@brampetersen lets keep the error open as a reminder to improve this!

[pjljvandelaar]

Changed title to better reflect isssue:
Parsing of SUT messages uses too little information: it doesn't use the expected type.
This lack of information can result in a MultipleDefinitions error as is shown in this issue!

[pjljvandelaar]

Note: In refactorAll branch is this problem absent, since

-- | 'TorXakis.Value.Value' from 'Data.Text.Text' conversion.
-- Expected 'TorXakis.Sort' of 'TorXakis.Value.Value' must be provided.
valueFromText :: SortContext c => c -> Sort -> Text -> Either Error Value