K-user mailing list

[Stephen Chang <stchang AT ccs.neu.edu>]

On Tue, Nov 15, 2011 at 2:58 PM, Chucky Ellison 
<celliso2 AT illinois.edu>
 wrote:
> Alright, try this please :)
>
> $ krun --log-io programs/diverse/factorial.simple
> $ cat krunner.log

stchang@caprica:~/k-framework/examples/languages/research/simple/untyped$
krun --log-io programs/diverse/factorial.simple
Unable to parse Maude's output:

Maude>

stchang@caprica:~/k-framework/examples/languages/research/simple/untyped$
cat krunner.log
Nov 15, 2011 3:00:14 PM runner.KRunner <init>
INFO: Maude and command files exist.
Nov 15, 2011 3:00:14 PM runner.KRunner startServer
INFO: Trying to start server on port 0
Nov 15, 2011 3:00:14 PM runner.KRunner startServer
INFO: Server started on port 53056
Nov 15, 2011 3:00:14 PM main.IOServer acceptConnections
INFO: Server started at 0.0.0.0/0.0.0.0: 53056
Nov 15, 2011 3:00:14 PM runner.KRunner run
INFO: Maude started
Nov 15, 2011 3:00:14 PM runner.KRunner run
INFO: Maude command:
load 
/home/stchang/k-framework/examples/languages/research/simple/untyped/simple-untyped-compiled.maude
mod KRUNNER is including SIMPLE-UNTYPED .
eq #TCPPORT = 53056 .
endm
load 
/home/stchang/k-framework/examples/languages/research/simple/untyped/.k/krun_tmp/maude_in



















>
> On Tue, Nov 15, 2011 at 1:34 PM, Stephen Chang 
> <stchang AT ccs.neu.edu>
>  wrote:
>> On Tue, Nov 15, 2011 at 2:26 PM, Chucky Ellison 
>> <celliso2 AT illinois.edu>
>>  wrote:
>>> Can you try
>>> (1)
>>> $ krun programs/diverse/factorial.simple
>>> again, just to make sure?
>>
>> stchang@caprica:~/k-framework/examples/languages/research/simple/untyped$
>> krun programs/diverse/factorial.simple
>> Unable to parse Maude's output:
>>
>> Maude>
>>
>>
>>
>>>
>>> If that still doesn't work, then please do
>>> (2)
>>> $ krun --no-io programs/diverse/div-nondet.simple
>>> and paste us your output, then
>>
>> stchang@caprica:~/k-framework/examples/languages/research/simple/untyped$
>> krun --no-io programs/diverse/div-nondet.simple
>> <T>
>>  <nextLoc>
>>    2
>>  </nextLoc>
>>  <in>
>>    .
>>  </in>
>>  <out>
>>    "1\n"
>>  </out>
>>  <threads>
>>    .
>>  </threads>
>>  <busy>
>>    .
>>  </busy>
>>  <genv>
>>    main |-> 0
>>  </genv>
>>  <store>
>>    0 |-> lambda( .List{","} , { var x , .List{","} ; ~> x = 1 ; ~>
>> print( ++ x / ++ x / x , "\n" , .List{","} ); } )
>>    1 |-> 3
>>  </store>
>> </T>
>>
>>
>>
>>> (3)
>>> $ maude simple-untyped-compiled.maude .k/krun_tmp/maude_in
>>> and paste us your output.
>>
>> stchang@caprica:~/k-framework/examples/languages/research/simple/untyped$
>> maude simple-untyped-compiled.maude .k/krun_tmp/maude_in
>>                     \||||||||||||||||||/
>>                   --- Welcome to Maude ---
>>                     /||||||||||||||||||\
>>            Maude 2.6 built: Dec  9 2010 18:28:39
>>            Copyright 1997-2010 SRI International
>>                   Tue Nov 15 14:33:46 2011
>> rewrites: 205 in 0ms cpu (0ms real) (~ rewrites/second)
>> result BagItem:
>> < T >
>>  < nextLoc > # 2(.List{K}) </ nextLoc >
>>  < in > #buffer(.) </ in >
>>  < out > #buffer(# "1\n"(.List{K})) </ out >
>>  < threads > (.).Bag </ threads >
>>  < busy > (.).Set </ busy >
>>  < genv > # #id "main"(.List{K}) |-> # 0(.List{K}) </ genv >
>>  < store > # 0(.List{K}) |-> 
>> 'lambda`(_`,_`)('.List`{","`}(.List{K}),,'`{_`}(
>>    'var_;('_`,_(# #id "x"(.List{K}),,'.List`{","`}(.List{K}))) ~> 
>> '_;('_=_(#
>>    #id "x"(.List{K}),,# 1(.List{K}))) ~> 'print`(_`);('_`,_('_/_('++_(# #id
>>    "x"(.List{K})),,'_/_('++_(# #id "x"(.List{K})),,# #id "x"(.List{K}))),,
>>    '_`,_(# "\n"(.List{K}),,'.List`{","`}(.List{K})))))) # 1(.List{K}) |-> 
>> # 3(
>>    .List{K}) </ store > </ T >
>> Bye.
>>
>>
>>
>>
>>
>>
>>>
>>> Thanks,
>>> -Chucky
>>>
>>> On Tue, Nov 15, 2011 at 1:17 PM, Stephen Chang 
>>> <stchang AT ccs.neu.edu>
>>>  wrote:
>>>> Thank you for all the help. It seems like the --search option did 
>>>> something.
>>>>
>>>>
>>>>
>>>> On Tue, Nov 15, 2011 at 2:10 PM, Chucky Ellison 
>>>> <celliso2 AT illinois.edu>
>>>>  wrote:
>>>>> Stephen, can you try running:
>>>>> $ echo "5" | krun --search programs/diverse/factorial.simple
>>>>> and paste the output
>>>>
>>>> stchang@caprica:~/k-framework/examples/languages/research/simple/untyped$
>>>> echo "5" | krun --search programs/diverse/factorial.simple
>>>> Search results:
>>>>
>>>> Solution 1, state 51:
>>>> <T>
>>>>  <nextLoc>
>>>>    5
>>>>  </nextLoc>
>>>>  <in>
>>>>    ""
>>>>  </in>
>>>>  <out>
>>>>    "Input a natural numer: Factorial of 5 is: 120\n"
>>>>  </out>
>>>>  <threads>
>>>>    .
>>>>  </threads>
>>>>  <busy>
>>>>    .
>>>>  </busy>
>>>>  <genv>
>>>>    factorial |-> 0
>>>>    main |-> 1
>>>>  </genv>
>>>>  <store>
>>>>    0 |-> lambda( y , .List{","} , { var t , .List{","} ; ~> t = 1 ;
>>>> ~> print( "Factorial of " , y , " is: " , .List{","} ); ~> { var i ,
>>>> .List{","} ; ~> i = 1 ; ~> while i <= y do { t = t * i ; ~> i = i + 1
>>>> ; } } ~> return t ; } )
>>>>    1 |-> lambda( .List{","} , { print( "Input a natural numer: " ,
>>>> .List{","} ); ~> print( factorial ( read() , .List{","} ) , "\n" ,
>>>> .List{","} ); } )
>>>>    2 |-> 5
>>>>    3 |-> 120
>>>>    4 |-> 6
>>>>  </store>
>>>> </T>
>>>>
>>>>
>>>>
>>>>
>>>>
>>>>> and then
>>>>> $ maude simple-untyped-compiled.maude .k/krun_tmp/maude_in
>>>>> and paste the output?
>>>>
>>>> stchang@caprica:~/k-framework/examples/languages/research/simple/untyped$
>>>> maude simple-untyped-compiled.maude .k/krun_tmp/maude_in
>>>>                     \||||||||||||||||||/
>>>>                   --- Welcome to Maude ---
>>>>                     /||||||||||||||||||\
>>>>            Maude 2.6 built: Dec  9 2010 18:28:39
>>>>            Copyright 1997-2010 SRI International
>>>>                   Tue Nov 15 14:15:02 2011
>>>> Advisory: socket manager declined malformed message 
>>>> #createClientTcpSocket(
>>>>    #socketManager, cnum(0), "localhost", #TCPPORT).
>>>> Advisory: socket manager declined malformed message 
>>>> #createClientTcpSocket(
>>>>    #socketManager, cnum(1), "localhost", #TCPPORT).
>>>> Advisory: socket manager declined malformed message 
>>>> #createClientTcpSocket(
>>>>    #socketManager, cnum(0), "localhost", #TCPPORT).
>>>> Advisory: socket manager declined malformed message 
>>>> #createClientTcpSocket(
>>>>    #socketManager, cnum(1), "localhost", #TCPPORT).
>>>> Advisory: socket manager declined malformed message 
>>>> #createClientTcpSocket(
>>>>    #socketManager, cnum(0), "localhost", #TCPPORT).
>>>> rewrites: 158 in 0ms cpu (1ms real) (~ rewrites/second)
>>>> result BagItem:
>>>> < T >
>>>>  < nextLoc > # 2(.List{K}) </ nextLoc >
>>>>  < in > #parse("#Int",.) ListItem('#charString`(_`)('#string2Int`(_`)(#
>>>>    #checkResult(#containedRequest(<> #Socket #toSend("1#readbyte#0#\r\n")
>>>>    #Socket < cnum(1) : Client | state: connecting > #Socket
>>>>    #createClientTcpSocket(#socketManager, cnum(1), "localhost", 
>>>> #TCPPORT)))(
>>>>    .List{K})))) #buffer(.) #istream(0) </ in >
>>>>  < out > #ostream(1) ListItem('String2DotK`(_`)(# #checkResult(
>>>>    #containedRequest(<> #Socket #toSend("0#writebyte#1#73#\r\n") #Socket 
>>>> <
>>>>    cnum(0) : Client | state: connecting > #Socket #createClientTcpSocket(
>>>>    #socketManager, cnum(0), "localhost", #TCPPORT)))(.List{K})))
>>>>    #removeCharUponAck #buffer(# "Input a natural numer: "(.List{K})) </ 
>>>> out >
>>>>  < threads >
>>>>  < thread >
>>>>   < k > 'read`(`)(.List{K}) ~> freezer('_`,_(var{K}("`[HOLE`]"),,var{K}(
>>>>    "K2")))(var{K}("K2")<-('.List`{","`}(.List{K}))) ~> 
>>>> freezer('_`(_`)(var{K}(
>>>>    "K1"),,var{K}("`[HOLE`]")))(var{K}("K1")<-(# #id 
>>>> "factorial"(.List{K}))) ~>
>>>>    
>>>> freezer('_`,_(var{K}("`[HOLE`]"),,var{K}("K2")))(var{K}("K2")<-('_`,_(#
>>>>    "\n"(.List{K}),,'.List`{","`}(.List{K})))) ~> 
>>>> freezer('print`(_`);(var{K}(
>>>>    "`[HOLE`]")))(.List{K}) ~> 'env`(_`)(wmap (# #id 
>>>> "factorial"(.List{K}) |->
>>>>    # 0(.List{K}) # #id "main"(.List{K}) |-> # 1(.List{K}))(.List{K})) ~>
>>>>    'return_;('nothing(.List{K})) </ k >
>>>>   < control >
>>>>    < fstack > (# #id "factorial"(.List{K}) |-> # 0(.List{K}) # #id 
>>>> "main"(
>>>>    .List{K}) |-> # 
>>>> 1(.List{K})),freezer('_;(var{K}("`[HOLE`]")))(.List{K}),
>>>>     < xstack > (.).List </ xstack > </ fstack >
>>>>    < xstack > (.).List </ xstack > </ control >
>>>>   < env > # #id "factorial"(.List{K}) |-> # 0(.List{K}) # #id 
>>>> "main"(.List{K})
>>>>    |-> # 1(.List{K}) </ env >
>>>>   < holds > (.).Map </ holds > </ thread > </ threads >
>>>>  < busy > (.).Set </ busy >
>>>>  < genv > # #id "factorial"(.List{K}) |-> # 0(.List{K}) # #id 
>>>> "main"(.List{K})
>>>>    |-> # 1(.List{K}) </ genv >
>>>>  < store > # 0(.List{K}) |-> 'lambda`(_`,_`)('_`,_(# #id "y"(.List{K}),,
>>>>    '.List`{","`}(.List{K})),,'`{_`}('var_;('_`,_(# #id "t"(.List{K}),,
>>>>    '.List`{","`}(.List{K}))) ~> '_;('_=_(# #id "t"(.List{K}),,# 
>>>> 1(.List{K})))
>>>>    ~> 'print`(_`);('_`,_(# "Factorial of "(.List{K}),,'_`,_(# #id 
>>>> "y"(.List{
>>>>    K}),,'_`,_(# " is: "(.List{K}),,'.List`{","`}(.List{K}))))) ~> '`{_`}(
>>>>    'var_;('_`,_(# #id "i"(.List{K}),,'.List`{","`}(.List{K}))) ~> 
>>>> '_;('_=_(#
>>>>    #id "i"(.List{K}),,# 1(.List{K}))) ~> 'while_do_('_<=_(# #id 
>>>> "i"(.List{K}),
>>>>    ,# #id "y"(.List{K})),,'`{_`}('_;('_=_(# #id "t"(.List{K}),,'_*_(# 
>>>> #id "t"(
>>>>    .List{K}),,# #id "i"(.List{K})))) ~> '_;('_=_(# #id 
>>>> "i"(.List{K}),,'_+_(#
>>>>    #id "i"(.List{K}),,# 1(.List{K}))))))) ~> 'return_;(# #id 
>>>> "t"(.List{K}))))
>>>>    # 1(.List{K}) |-> 'lambda`(_`,_`)('.List`{","`}(.List{K}),,'`{_`}(
>>>>    'print`(_`);('_`,_(# "Input a natural numer: 
>>>> "(.List{K}),,'.List`{","`}(
>>>>    .List{K}))) ~> 'print`(_`);('_`,_('_`(_`)(# #id 
>>>> "factorial"(.List{K}),,
>>>>    '_`,_('read`(`)(.List{K}),,'.List`{","`}(.List{K}))),,'_`,_(# 
>>>> "\n"(.List{
>>>>    K}),,'.List`{","`}(.List{K})))))) </ store > </ T >
>>>> Bye.
>>>>
>>>
>>
>