K-user mailing list

[Dorel Lucanu <dlucanu AT info.uaic.ro>]

The options --superheat and --supercool are useless here because no 
heating/cooling rules are involved.
Just try to add the label "eout" to the --transition argument.

Dorel

On 26/01/16 03:45, 
davidistreader AT gmail.com
 wrote:
> Any suggestions about what to read?
>
> In particular K rules can be conditional   ...... "requires"  Boolean
>
> is there any way to make a rule conditional on  some thing not being in a Map
> or a Set?
>
> And from some reading it seems that conditional rules are best avoided is that
> so?
>
> I am interested in SOS definitions of process algebra.
>
>   rule <k> evt N:String -> P:Process => P</k>
>         <evt> ... .List => ListItem(N) </evt>  [events ]
>
> To introduce the external nondeterminism  I can see no way of saying
> if P-a->Q then (P+R)->Q  so I tried
>
>     rule <k> P:Process + Q:Process => Q</k> [structural, eout]
>     rule <k> P:Process + Q:Process => P</k> [structural, eout]
>
> but this did not work  as expected with
>
> kompile --transition "events” —-superheat “plus” --supercool  “eout"  proc.k
>
> krun --search one.proc
>
> Any ideas -- This might be very very wrong but hints welcome