K-user mailing list

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

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.