Skip to Content.
Sympa Menu

k-user - Re: [[K-user] ] Staging the evaluation of rules

k-user AT lists.cs.illinois.edu

Subject: K-user mailing list

List archive

Re: [[K-user] ] Staging the evaluation of rules


Chronological Thread 
  • From: Daniel Schnetzer Fava <danielsf AT ifi.uio.no>
  • To: Markus Knecht <markus.knecht85 AT gmail.com>
  • Cc: "k-user AT lists.cs.illinois.edu" <k-user AT lists.cs.illinois.edu>, "Daniel Schnetzer Fava" <danielsf AT ifi.uio.no>
  • Subject: Re: [[K-user] ] Staging the evaluation of rules
  • Date: Fri, 5 Jan 2018 14:03:02 +0000
  • Accept-language: en-US, nb-NO
  • Authentication-results: illinois.edu; spf=pass smtp.mailfrom=danielsf AT ifi.uio.no

It seems like it is not recognizing BQ as a list.
If I replace size(BQ) with size(.List), it rewrites size(.List) to 0.

  rule <k> IsSelBranchEnabled( let Z:Id = channel(Ref:Int) <- V:Val in T:Term ) => size(.List) ... </k>

Daniel


On 5 Jan 2018, at 14:13, Daniel Schnetzer Fava <danielsf AT ifi.uio.no> wrote:


  rule <k> IsSelBranchEnabled( let Z:Id = channel(Ref:Int) <- V:Val in T:Term ) => size(BQ) ... </k>

the result is simply: size(BQ)

More specifically, the result is:
<k> size ( ListItem ( ListItem ( 42 ) ListItem ( .Map ) ListItem ( .Set ) ) ) </k>



On 5 Jan 2018, at 14:07, Daniel Schnetzer Fava <danielsf AT ifi.uio.no> wrote:

Seems like size(BQ) is not being evaluated.

If I replace:
  rule <k> IsSelBranchEnabled( let Z:Id = channel(Ref:Int) <- V:Val in T:Term ) => size(BQ) >=Int 1 ... </k>

by:
  rule <k> IsSelBranchEnabled( let Z:Id = channel(Ref:Int) <- V:Val in T:Term ) => size(BQ) ... </k>

the result is simply: size(BQ)

But if I replace it by
  rule <k> IsSelBranchEnabled( let Z:Id = channel(Ref:Int) <- V:Val in T:Term ) => 0 >=Int 1 ... </k>

the result is “false” as expected.

Daniel


On 5 Jan 2018, at 11:39, Markus Knecht <markus.knecht85 AT gmail.com> wrote:

It seems that 
size ( ListItem ( ListItem ( 42 ) ListItem ( .Map ) ListItem ( .Set ) ) )
cannot be evaluated and thus >=Int is stuck, the question is why, I do not see it, especially as you have the same _expression_ size(BQ) in the requires where it seems to work.
It may have something to do that Int >=Int Int is already a Bool even in its unevaluated form, but that is unlikely as Int >=Int Int is defined as a function and should match anywhere anyways.
If you use:
rule <k> R:Bool ~> selFindEnBs(BTail, L) => selFindEnBs(BTail, L ListItem(R)) </k>
Instead of the true/false version, does the unevaluated Term end up in the ListItem of selFindEnBs ? atleast the rewriting would continue but will be stuck later, so no solution but maybe it helps pinpoint the problem.

Daniel Schnetzer Fava <danielsf AT ifi.uio.no> schrieb am Fr., 5. Jan. 2018 um 11:13 Uhr:
Hi Markus,

Thanks for the reply.

What error do you get?
Does the evaluation get Stuck at   aBoolean  ~> selFindEnBs(...) , or does IsSelBranchEnabled(BHead) fails to evaluate to a boolean? or did it not kompile at all? 

IsSelBranchEnabled(BHead) fails to evaluate to a boolean.

It does get evaluated to a certain degree, but it stops here, and does not evaluate the >=Int

size ( ListItem ( ListItem ( 42 ) ListItem ( .Map ) ListItem ( .Set ) ) ) >=Int 1

Here is the rule for IsSelBranchEnabled:

  syntax Bool ::= "IsSelBranchEnabled" "(" GChan ")"
  rule <k> IsSelBranchEnabled( let Z:Id = channel(Ref:Int) <- V:Val in T:Term ) => size(BQ) >=Int 1 ... </k>
      <chan>
        <ref> Ref </ref>
        <type> _ </type>
       <forward> FQ </forward>
       <backward> BQ </backward>
     </chan>
      requires (EotInFQ(FQ) ==Bool false) // channel is open  
               andBool
               (size(FQ) +Int size(BQ) >Int 0) // channel is async


   is Bool declared as KResult [do you have syntax KResult ::= Bool somwhere]

Bool is declared as KResult.

Thanks again,

Daniel

PS.
Independent tips:
  I don't think the brackets before => are necessary
  instead of true/false ~> ... you could capture both in one statement with Res:Bool ~> …

Great!  I appreciate the comments.  Often, even though I manage to accomplish what I need/want, I get the feeling that there is a better way of doing it.


On 4 Jan 2018, at 16:55, Markus Knecht <markus.knecht85 AT gmail.com> wrote:

What error do you get?
Does the evaluation get Stuck at   aBoolean  ~> selFindEnBs(...) , or does IsSelBranchEnabled(BHead) fails to evaluate to a boolean? or did it not kompile at all? 

Some things to check: 
   if something follows selFindEnBs you need to add ... before  </k>. 
   is Bool declared as KResult [do you have syntax KResult ::= Bool somwhere]

Independent tips:
  I don't think the brackets before => are necessary
  instead of true/false ~> ... you could capture both in one statement with Res:Bool ~> ...


Daniel Schnetzer Fava <danielsf AT ifi.uio.no> schrieb am Do., 4. Jan. 2018 um 16:25 Uhr:
Hi,

I am trying to write a rule that first evaluates another, then evaluates itself.
I think I ought to be using ~> but I am not sure exactly how.

Here is some attempt that does not seem to work:

rule <k> selFindEnBs({ BHead } BTail, L:List) =>
            IsSelBranchEnabled(BHead) ~> selFindEnBs(BTail, L) </k>
rule <k> (true ~> selFindEnBs(BTail, L)) => 
              selFindEnBs(BTail, L ListItem(true)) </k>
rule <k> (false ~> selFindEnBs(BTail, L)) => 
              selFindEnBs(BTail, L ListItem(false)) </k>

The goal is to have the result of “IsSelBranchEnabled(BHead)” appended to the list L
and then continue evaluating selFindEnBs on BTail.

Any help is highly appreciated!

Thanks,

Daniel







Archive powered by MHonArc 2.6.24.

Top of Page