k-user AT lists.cs.illinois.edu

Subject: K-user mailing list

List archive

[[K-user] ] [Error] Critical: No operator registered

From: Gurvan Le Guernic <gleguern AT gmail.com>
To: k-user AT cs.uiuc.edu
Subject: [[K-user] ] [Error] Critical: No operator registered
Date: Fri, 21 Feb 2020 14:59:48 +0100
Authentication-results: illinois.edu; spf=softfail smtp.mailfrom=gleguern AT gmail.com; dkim=pass header.d=gmail.com header.s=20161025; dmarc=pass header.from=gmail.com

Hi,

What does "[Error] Critical: No operator registered for closing cells of sort TransitionSet when closing cell" mean ? I tried to Google it but did not found any explanations.

I have the following definitions:

syntax Transition ::= StateIdSet "-{" Trigger "|" ActionsList "}->" StateIdSet
syntax TransitionSet ::= Set

A the following rule fragment:

<transitions> ... SetItem( FSs -{ None | As:ActionsList }-> TSs:StateIdSet ) ... </transitions>

The <transition> cell contains a TransitionSet.

I get the following compilation error :

org.kframework.utils.errorsystem.KEMException: [Error] Critical: No operator registered for closing cells of sort TransitionSet when closing cell `<transitions>`(#dots(.KList),`SetItem`(`_-{_|_}->__ENVIRONMENT-ABSTRACT-SYNTAX_Transition_StateIdSet_Trigger_ActionsList_StateIdSet`(FSs,`None_ENVIRONMENT-ABSTRACT-SYNTAX_Trigger`(.KList),As,TSs)),#dots(.KList))
while executing phase "concretizing configuration" on sentence at ...

Any idea how to fix such errors ?

Thanks,

[[K-user] ] [Error] Critical: No operator registered, Gurvan Le Guernic, 02/21/2020