owl.*
-
owl.Bibliography Modifier and Type Constant Field Value public static final StringATVA_18_CITEKEY"KMS18"public static final StringATVA_19_CITEKEY"LP19a"public static final StringCAV_16_CITEKEY"SEJK16"public static final StringCAV_18_CITEKEY"KMSZ18"public static final StringDISSERTATION_19_CITEKEY"S19"public static final StringFMSD_16_CITEKEY"EKS16"public static final StringFSTTCS_10_CITEKEY"BKS10"public static final StringGANDALF_17_CITEKEY"MS17"public static final StringICALP_19_1_CITEKEY"LP19b"public static final StringICALP_19_2_CITEKEY"AK19"public static final StringICALP_21_CITEKEY"CCF21"public static final StringJACM_20_CITEKEY"EKS20"public static final StringJACM_95_CITEKEY"CY95"public static final StringLICS_18_CITEKEY"EKS18"public static final StringLICS_20_CITEKEY"SE20"public static final StringTACAS_17_1_CITEKEY"EKRS17"public static final StringTACAS_17_2_CITEKEY"KMWW17"public static final StringUNDER_SUBMISSION_21_CITEKEY"SLM21"public static final StringUNDER_SUBMISSION_22_CITEKEY"CDMRS22"
owl.cinterface.*
-
owl.cinterface.CInterface Modifier and Type Constant Field Value public static final StringCALL_DESTROY"This function returns a void pointer to an opaque Java object handle. The object is not collected by the garbage collected unless \'destroy_object_handle\' is called on the pointer."public static final StringCHAR_TO_STRING"Decodes a 0 terminated C char* to a Java string using the platform\'s default charset."public static final intFEATURE_SEPARATOR-424242public static final intSEPARATOR-232323
owl.grammar.*
-
owl.grammar.LTLLexer Modifier and Type Constant Field Value public static final String_serializedATN"\u0003\u608b\ua72a\u8133\ub9ed\u417c\u3be7\u7786\u5964\u0002\u001c\u00c6\b\u0001\b\u0001\b\u0001\u0004\u0002\t\u0002\u0004\u0003\t\u0003\u0004\u0004\t\u0004\u0004\u0005\t\u0005\u0004\u0006\t\u0006\u0004\u0007\t\u0007\u0004\b\t\b\u0004\t\t\t\u0004\n\t\n\u0004\u000b\t\u000b\u0004\f\t\f\u0004\r\t\r\u0004\u000e\t\u000e\u0004\u000f\t\u000f\u0004\u0010\t\u0010\u0004\u0011\t\u0011\u0004\u0012\t\u0012\u0004\u0013\t\u0013\u0004\u0014\t\u0014\u0004\u0015\t\u0015\u0004\u0016\t\u0016\u0004\u0017\t\u0017\u0004\u0018\t\u0018\u0004\u0019\t\u0019\u0004\u001a\t\u001a\u0004\u001b\t\u001b\u0004\u001c\t\u001c\u0003\u0002\u0003\u0002\u0003\u0002\u0003\u0002\u0003\u0002\u0003\u0002\u0003\u0002\u0005\u0002C\n\u0002\u0003\u0003\u0003\u0003\u0003\u0003\u0003\u0003\u0003\u0003\u0003\u0003\u0003\u0003\u0003\u0003\u0005\u0003M\n\u0003\u0003\u0004\u0003\u0004\u0003\u0004\u0003\u0004\u0005\u0004S\n\u0004\u0003\u0005\u0003\u0005\u0003\u0005\u0003\u0005\u0003\u0005\u0003\u0005\u0003\u0005\u0003\u0005\u0003\u0005\u0003\u0005\u0003\u0005\u0003\u0005\u0003\u0005\u0005\u0005b\n\u0005\u0003\u0006\u0003\u0006\u0003\u0006\u0003\u0006\u0003\u0006\u0003\u0006\u0003\u0006\u0003\u0006\u0003\u0006\u0003\u0006\u0003\u0006\u0005\u0006o\n\u0006\u0003\u0007\u0003\u0007\u0003\u0007\u0003\u0007\u0003\u0007\u0003\u0007\u0003\u0007\u0005\u0007x\n\u0007\u0003\b\u0003\b\u0003\b\u0003\b\u0003\b\u0003\b\u0005\b\u0080\n\b\u0003\t\u0003\t\u0003\t\u0003\t\u0003\t\u0005\t\u0087\n\t\u0003\n\u0003\n\u0003\u000b\u0003\u000b\u0003\f\u0003\f\u0003\r\u0003\r\u0003\u000e\u0003\u000e\u0003\u000f\u0003\u000f\u0003\u0010\u0003\u0010\u0003\u0011\u0003\u0011\u0003\u0012\u0003\u0012\u0003\u0013\u0003\u0013\u0003\u0013\u0003\u0013\u0003\u0014\u0003\u0014\u0003\u0014\u0003\u0014\u0003\u0015\u0003\u0015\u0007\u0015\u00a5\n\u0015\f\u0015\u000e\u0015\u00a8\u000b\u0015\u0003\u0016\u0006\u0016\u00ab\n\u0016\r\u0016\u000e\u0016\u00ac\u0003\u0017\u0003\u0017\u0003\u0017\u0003\u0017\u0003\u0018\u0003\u0018\u0003\u0018\u0003\u0018\u0003\u0019\u0006\u0019\u00b8\n\u0019\r\u0019\u000e\u0019\u00b9\u0003\u001a\u0003\u001a\u0003\u001a\u0003\u001a\u0003\u001b\u0006\u001b\u00c1\n\u001b\r\u001b\u000e\u001b\u00c2\u0003\u001c\u0003\u001c\u0002\u0002\u001d\u0005\u0003\u0007\u0004\t\u0005\u000b\u0006\r\u0007\u000f\b\u0011\t\u0013\n\u0015\u000b\u0017\f\u0019\r\u001b\u000e\u001d\u000f\u001f\u0010!\u0011#\u0012%\u0013\'\u0014)\u0015+\u0016-\u0002/\u00171\u00183\u00195\u001a7\u001b9\u001c\u0005\u0002\u0003\u0004\u0007\u0005\u0002NNaac|\u0006\u00022;C\\aac|\u0005\u0002\u000b\f\u000e\u000f\"\"\u0003\u0002$$\u0003\u0002))\u0002\u00d7\u0002\u0005\u0003\u0002\u0002\u0002\u0002\u0007\u0003\u0002\u0002\u0002\u0002\t\u0003\u0002\u0002\u0002\u0002\u000b\u0003\u0002\u0002\u0002\u0002\r\u0003\u0002\u0002\u0002\u0002\u000f\u0003\u0002\u0002\u0002\u0002\u0011\u0003\u0002\u0002\u0002\u0002\u0013\u0003\u0002\u0002\u0002\u0002\u0015\u0003\u0002\u0002\u0002\u0002\u0017\u0003\u0002\u0002\u0002\u0002\u0019\u0003\u0002\u0002\u0002\u0002\u001b\u0003\u0002\u0002\u0002\u0002\u001d\u0003\u0002\u0002\u0002\u0002\u001f\u0003\u0002\u0002\u0002\u0002!\u0003\u0002\u0002\u0002\u0002#\u0003\u0002\u0002\u0002\u0002%\u0003\u0002\u0002\u0002\u0002\'\u0003\u0002\u0002\u0002\u0002)\u0003\u0002\u0002\u0002\u0002+\u0003\u0002\u0002\u0002\u0002/\u0003\u0002\u0002\u0002\u00029\u0003\u0002\u0002\u0002\u00031\u0003\u0002\u0002\u0002\u00033\u0003\u0002\u0002\u0002\u00045\u0003\u0002\u0002\u0002\u00047\u0003\u0002\u0002\u0002\u0005B\u0003\u0002\u0002\u0002\u0007L\u0003\u0002\u0002\u0002\tR\u0003\u0002\u0002\u0002\u000ba\u0003\u0002\u0002\u0002\rn\u0003\u0002\u0002\u0002\u000fw\u0003\u0002\u0002\u0002\u0011\u007f\u0003\u0002\u0002\u0002\u0013\u0086\u0003\u0002\u0002\u0002\u0015\u0088\u0003\u0002\u0002\u0002\u0017\u008a\u0003\u0002\u0002\u0002\u0019\u008c\u0003\u0002\u0002\u0002\u001b\u008e\u0003\u0002\u0002\u0002\u001d\u0090\u0003\u0002\u0002\u0002\u001f\u0092\u0003\u0002\u0002\u0002!\u0094\u0003\u0002\u0002\u0002#\u0096\u0003\u0002\u0002\u0002%\u0098\u0003\u0002\u0002\u0002\'\u009a\u0003\u0002\u0002\u0002)\u009e\u0003\u0002\u0002\u0002+\u00a2\u0003\u0002\u0002\u0002-\u00aa\u0003\u0002\u0002\u0002/\u00ae\u0003\u0002\u0002\u00021\u00b2\u0003\u0002\u0002\u00023\u00b7\u0003\u0002\u0002\u00025\u00bb\u0003\u0002\u0002\u00027\u00c0\u0003\u0002\u0002\u00029\u00c4\u0003\u0002\u0002\u0002;<\u0007v\u0002\u0002<C\u0007v\u0002\u0002=>\u0007v\u0002\u0002>?\u0007t\u0002\u0002?@\u0007w\u0002\u0002@C\u0007g\u0002\u0002AC\u00073\u0002\u0002B;\u0003\u0002\u0002\u0002B=\u0003\u0002\u0002\u0002BA\u0003\u0002\u0002\u0002C\u0006\u0003\u0002\u0002\u0002DE\u0007h\u0002\u0002EM\u0007h\u0002\u0002FG\u0007h\u0002\u0002GH\u0007c\u0002\u0002HI\u0007n\u0002\u0002IJ\u0007u\u0002\u0002JM\u0007g\u0002\u0002KM\u00072\u0002\u0002LD\u0003\u0002\u0002\u0002LF\u0003\u0002\u0002\u0002LK\u0003\u0002\u0002\u0002M\b\u0003\u0002\u0002\u0002NS\u0007#\u0002\u0002OP\u0007P\u0002\u0002PQ\u0007Q\u0002\u0002QS\u0007V\u0002\u0002RN\u0003\u0002\u0002\u0002RO\u0003\u0002\u0002\u0002S\n\u0003\u0002\u0002\u0002TU\u0007/\u0002\u0002Ub\u0007@\u0002\u0002VW\u0007/\u0002\u0002WX\u0007/\u0002\u0002Xb\u0007@\u0002\u0002YZ\u0007?\u0002\u0002Zb\u0007@\u0002\u0002[\\\u0007?\u0002\u0002\\]\u0007?\u0002\u0002]b\u0007@\u0002\u0002^_\u0007K\u0002\u0002_`\u0007O\u0002\u0002`b\u0007R\u0002\u0002aT\u0003\u0002\u0002\u0002aV\u0003\u0002\u0002\u0002aY\u0003\u0002\u0002\u0002a[\u0003\u0002\u0002\u0002a^\u0003\u0002\u0002\u0002b\f\u0003\u0002\u0002\u0002cd\u0007>\u0002\u0002de\u0007/\u0002\u0002eo\u0007@\u0002\u0002fg\u0007>\u0002\u0002gh\u0007?\u0002\u0002ho\u0007@\u0002\u0002ij\u0007D\u0002\u0002jk\u0007K\u0002\u0002kl\u0007K\u0002\u0002lm\u0007O\u0002\u0002mo\u0007R\u0002\u0002nc\u0003\u0002\u0002\u0002nf\u0003\u0002\u0002\u0002ni\u0003\u0002\u0002\u0002o\u000e\u0003\u0002\u0002\u0002px\u0007`\u0002\u0002qr\u0007Z\u0002\u0002rs\u0007Q\u0002\u0002sx\u0007T\u0002\u0002tu\u0007z\u0002\u0002uv\u0007q\u0002\u0002vx\u0007t\u0002\u0002wp\u0003\u0002\u0002\u0002wq\u0003\u0002\u0002\u0002wt\u0003\u0002\u0002\u0002x\u0010\u0003\u0002\u0002\u0002yz\u0007(\u0002\u0002z\u0080\u0007(\u0002\u0002{\u0080\u0007(\u0002\u0002|}\u0007C\u0002\u0002}~\u0007P\u0002\u0002~\u0080\u0007F\u0002\u0002\u007fy\u0003\u0002\u0002\u0002\u007f{\u0003\u0002\u0002\u0002\u007f|\u0003\u0002\u0002\u0002\u0080\u0012\u0003\u0002\u0002\u0002\u0081\u0082\u0007~\u0002\u0002\u0082\u0087\u0007~\u0002\u0002\u0083\u0087\u0007~\u0002\u0002\u0084\u0085\u0007Q\u0002\u0002\u0085\u0087\u0007T\u0002\u0002\u0086\u0081\u0003\u0002\u0002\u0002\u0086\u0083\u0003\u0002\u0002\u0002\u0086\u0084\u0003\u0002\u0002\u0002\u0087\u0014\u0003\u0002\u0002\u0002\u0088\u0089\u0007H\u0002\u0002\u0089\u0016\u0003\u0002\u0002\u0002\u008a\u008b\u0007I\u0002\u0002\u008b\u0018\u0003\u0002\u0002\u0002\u008c\u008d\u0007Z\u0002\u0002\u008d\u001a\u0003\u0002\u0002\u0002\u008e\u008f\u0007W\u0002\u0002\u008f\u001c\u0003\u0002\u0002\u0002\u0090\u0091\u0007Y\u0002\u0002\u0091\u001e\u0003\u0002\u0002\u0002\u0092\u0093\u0007T\u0002\u0002\u0093 \u0003\u0002\u0002\u0002\u0094\u0095\u0007O\u0002\u0002\u0095\"\u0003\u0002\u0002\u0002\u0096\u0097\u0007*\u0002\u0002\u0097$\u0003\u0002\u0002\u0002\u0098\u0099\u0007+\u0002\u0002\u0099&\u0003\u0002\u0002\u0002\u009a\u009b\u0007$\u0002\u0002\u009b\u009c\u0003\u0002\u0002\u0002\u009c\u009d\b\u0013\u0002\u0002\u009d(\u0003\u0002\u0002\u0002\u009e\u009f\u0007)\u0002\u0002\u009f\u00a0\u0003\u0002\u0002\u0002\u00a0\u00a1\b\u0014\u0003\u0002\u00a1*\u0003\u0002\u0002\u0002\u00a2\u00a6\t\u0002\u0002\u0002\u00a3\u00a5\t\u0003\u0002\u0002\u00a4\u00a3\u0003\u0002\u0002\u0002\u00a5\u00a8\u0003\u0002\u0002\u0002\u00a6\u00a4\u0003\u0002\u0002\u0002\u00a6\u00a7\u0003\u0002\u0002\u0002\u00a7,\u0003\u0002\u0002\u0002\u00a8\u00a6\u0003\u0002\u0002\u0002\u00a9\u00ab\t\u0004\u0002\u0002\u00aa\u00a9\u0003\u0002\u0002\u0002\u00ab\u00ac\u0003\u0002\u0002\u0002\u00ac\u00aa\u0003\u0002\u0002\u0002\u00ac\u00ad\u0003\u0002\u0002\u0002\u00ad.\u0003\u0002\u0002\u0002\u00ae\u00af\u0005-\u0016\u0002\u00af\u00b0\u0003\u0002\u0002\u0002\u00b0\u00b1\b\u0017\u0004\u0002\u00b10\u0003\u0002\u0002\u0002\u00b2\u00b3\u0007$\u0002\u0002\u00b3\u00b4\u0003\u0002\u0002\u0002\u00b4\u00b5\b\u0018\u0005\u0002\u00b52\u0003\u0002\u0002\u0002\u00b6\u00b8\n\u0005\u0002\u0002\u00b7\u00b6\u0003\u0002\u0002\u0002\u00b8\u00b9\u0003\u0002\u0002\u0002\u00b9\u00b7\u0003\u0002\u0002\u0002\u00b9\u00ba\u0003\u0002\u0002\u0002\u00ba4\u0003\u0002\u0002\u0002\u00bb\u00bc\u0007)\u0002\u0002\u00bc\u00bd\u0003\u0002\u0002\u0002\u00bd\u00be\b\u001a\u0005\u0002\u00be6\u0003\u0002\u0002\u0002\u00bf\u00c1\n\u0006\u0002\u0002\u00c0\u00bf\u0003\u0002\u0002\u0002\u00c1\u00c2\u0003\u0002\u0002\u0002\u00c2\u00c0\u0003\u0002\u0002\u0002\u00c2\u00c3\u0003\u0002\u0002\u0002\u00c38\u0003\u0002\u0002\u0002\u00c4\u00c5\u000b\u0002\u0002\u0002\u00c5:\u0003\u0002\u0002\u0002\u0011\u0002\u0003\u0004BLRanw\u007f\u0086\u00a6\u00ac\u00b9\u00c2\u0006\u0004\u0003\u0002\u0004\u0004\u0002\b\u0002\u0002\u0004\u0002\u0002"public static final intAND7public static final intBIIMP5public static final intDOUBLE_QUOTED1public static final intDOUBLE_QUOTED_VARIABLE23public static final intERROR26public static final intFALSE2public static final intFINALLY9public static final intGLOBALLY10public static final intIMP4public static final intLDQUOTE18public static final intLPAREN16public static final intLSQUOTE19public static final intNEXT11public static final intNOT3public static final intOR8public static final intRDQUOTE22public static final intRELEASE14public static final intRPAREN17public static final intRSQUOTE24public static final intSINGLE_QUOTED2public static final intSINGLE_QUOTED_VARIABLE25public static final intSKIP_DEF21public static final intSRELEASE15public static final intTRUE1public static final intUNTIL12public static final intVARIABLE20public static final intWUNTIL13public static final intXOR6 -
owl.grammar.LTLParser Modifier and Type Constant Field Value public static final String_serializedATN"\u0003\u608b\ua72a\u8133\ub9ed\u417c\u3be7\u7786\u5964\u0003\u001cM\u0004\u0002\t\u0002\u0004\u0003\t\u0003\u0004\u0004\t\u0004\u0004\u0005\t\u0005\u0004\u0006\t\u0006\u0004\u0007\t\u0007\u0004\b\t\b\u0004\t\t\t\u0004\n\t\n\u0004\u000b\t\u000b\u0003\u0002\u0003\u0002\u0003\u0002\u0003\u0003\u0003\u0003\u0003\u0004\u0003\u0004\u0003\u0004\u0007\u0004\u001f\n\u0004\f\u0004\u000e\u0004\"\u000b\u0004\u0003\u0005\u0003\u0005\u0003\u0005\u0007\u0005\'\n\u0005\f\u0005\u000e\u0005*\u000b\u0005\u0003\u0006\u0003\u0006\u0003\u0006\u0003\u0006\u0003\u0006\u0005\u00061\n\u0006\u0003\u0007\u0003\u0007\u0003\u0007\u0003\u0007\u0005\u00077\n\u0007\u0003\b\u0003\b\u0003\b\u0003\b\u0003\b\u0003\b\u0003\b\u0003\b\u0003\b\u0003\b\u0003\b\u0003\b\u0005\bE\n\b\u0003\t\u0003\t\u0003\n\u0003\n\u0003\u000b\u0003\u000b\u0003\u000b\u0002\u0002\f\u0002\u0004\u0006\b\n\f\u000e\u0010\u0012\u0014\u0002\u0005\u0004\u0002\u0005\u0005\u000b\r\u0004\u0002\u0006\b\u000e\u0011\u0003\u0002\u0003\u0004\u0002J\u0002\u0016\u0003\u0002\u0002\u0002\u0004\u0019\u0003\u0002\u0002\u0002\u0006\u001b\u0003\u0002\u0002\u0002\b#\u0003\u0002\u0002\u0002\n0\u0003\u0002\u0002\u0002\f6\u0003\u0002\u0002\u0002\u000eD\u0003\u0002\u0002\u0002\u0010F\u0003\u0002\u0002\u0002\u0012H\u0003\u0002\u0002\u0002\u0014J\u0003\u0002\u0002\u0002\u0016\u0017\u0005\u0004\u0003\u0002\u0017\u0018\u0007\u0002\u0002\u0003\u0018\u0003\u0003\u0002\u0002\u0002\u0019\u001a\u0005\u0006\u0004\u0002\u001a\u0005\u0003\u0002\u0002\u0002\u001b \u0005\b\u0005\u0002\u001c\u001d\u0007\n\u0002\u0002\u001d\u001f\u0005\b\u0005\u0002\u001e\u001c\u0003\u0002\u0002\u0002\u001f\"\u0003\u0002\u0002\u0002 \u001e\u0003\u0002\u0002\u0002 !\u0003\u0002\u0002\u0002!\u0007\u0003\u0002\u0002\u0002\" \u0003\u0002\u0002\u0002#(\u0005\n\u0006\u0002$%\u0007\t\u0002\u0002%\'\u0005\n\u0006\u0002&$\u0003\u0002\u0002\u0002\'*\u0003\u0002\u0002\u0002(&\u0003\u0002\u0002\u0002()\u0003\u0002\u0002\u0002)\t\u0003\u0002\u0002\u0002*(\u0003\u0002\u0002\u0002+,\u0005\f\u0007\u0002,-\u0005\u0012\n\u0002-.\u0005\n\u0006\u0002.1\u0003\u0002\u0002\u0002/1\u0005\f\u0007\u00020+\u0003\u0002\u0002\u00020/\u0003\u0002\u0002\u00021\u000b\u0003\u0002\u0002\u000223\u0005\u0010\t\u000234\u0005\n\u0006\u000247\u0003\u0002\u0002\u000257\u0005\u000e\b\u000262\u0003\u0002\u0002\u000265\u0003\u0002\u0002\u00027\r\u0003\u0002\u0002\u00028E\u0005\u0014\u000b\u00029E\u0007\u0016\u0002\u0002:;\u0007\u0015\u0002\u0002;<\u0007\u001b\u0002\u0002<E\u0007\u001a\u0002\u0002=>\u0007\u0014\u0002\u0002>?\u0007\u0019\u0002\u0002?E\u0007\u0018\u0002\u0002@A\u0007\u0012\u0002\u0002AB\u0005\u0004\u0003\u0002BC\u0007\u0013\u0002\u0002CE\u0003\u0002\u0002\u0002D8\u0003\u0002\u0002\u0002D9\u0003\u0002\u0002\u0002D:\u0003\u0002\u0002\u0002D=\u0003\u0002\u0002\u0002D@\u0003\u0002\u0002\u0002E\u000f\u0003\u0002\u0002\u0002FG\t\u0002\u0002\u0002G\u0011\u0003\u0002\u0002\u0002HI\t\u0003\u0002\u0002I\u0013\u0003\u0002\u0002\u0002JK\t\u0004\u0002\u0002K\u0015\u0003\u0002\u0002\u0002\u0007 (06D"public static final intAND7public static final intBIIMP5public static final intDOUBLE_QUOTED_VARIABLE23public static final intERROR26public static final intFALSE2public static final intFINALLY9public static final intGLOBALLY10public static final intIMP4public static final intLDQUOTE18public static final intLPAREN16public static final intLSQUOTE19public static final intNEXT11public static final intNOT3public static final intOR8public static final intRDQUOTE22public static final intRELEASE14public static final intRPAREN17public static final intRSQUOTE24public static final intRULE_andExpression3public static final intRULE_atomExpression6public static final intRULE_binaryExpression4public static final intRULE_binaryOp8public static final intRULE_bool9public static final intRULE_expression1public static final intRULE_formula0public static final intRULE_orExpression2public static final intRULE_unaryExpression5public static final intRULE_unaryOp7public static final intSINGLE_QUOTED_VARIABLE25public static final intSKIP_DEF21public static final intSRELEASE15public static final intTRUE1public static final intUNTIL12public static final intVARIABLE20public static final intWUNTIL13public static final intXOR6
owl.ltl.*
-
owl.ltl.rewriter.LiteralMapper Modifier and Type Constant Field Value public static final intUNDEFINED-1
owl.translations.*
-
owl.translations.LtlTranslationRepository.LtlToDelaTranslation Modifier and Type Constant Field Value public static final StringMS17_DESCRIPTION"Translate the formula to a deterministic Emerson-Lei automaton using an specialised product construction and a portfolio of constructions for simple LTL fragments. This construction has been originally be implemented in \'delag\' and presented in [MS17]. If a subformula is not in a supported fragment then [EKS20] is used as a fallback."public static final StringSLM21_DESCRIPTION"Translate the formula to a deterministic Emerson-Lei automaton by rewriting the formula locally into the \u0394\u2082-normalform using the procedure of [SE20], i.e., only temporal subformulas that are not in \u0394\u2082 are rewritten, and then use an specialised product construction [SLM21] to obtain a deterministic automaton. After rewriting each temporal subformula is in \u03a3\u2082 or \u03a0\u2082 and the direct translation to deterministic co-B\u00fcchi and B\u00fcchi automata from [SLM21] is sufficient."public static final StringSMALLEST_AUTOMATON_DESCRIPTION"Run all available DELA- and DGRA-translations with all optimisations turned on in parallel and return the smallest automaton." -
owl.translations.LtlTranslationRepository.LtlToDpaTranslation Modifier and Type Constant Field Value public static final StringEKS20_EKRS17_DESCRIPTION"Translate the formula to a deterministic parity automaton by combining [EKS20] with the LDBA-to-DPA translation of [EKRS17]. This translation used to be available through the \'--symmetric\' option."public static final StringSEJK16_EKRS17_DESCRIPTION"Translate the formula to a deterministic parity automaton by combining [SEJK16] with the LDBA-to-DPA translation of [EKRS17]. This translation used to be available through the \'--asymmetric\' option."public static final StringSLM21_DESCRIPTION"Translate the formula to a deterministic parity automaton by combining the LTL-to-DELA translation of [SLM21] with a DELW-to-DPW translation based on Zielonka-trees. Depending on the lookahead either [CCF21] or [SLM21] is used."public static final StringSMALLEST_AUTOMATON_DESCRIPTION"Run all available DPA-translations with all optimisations turned on in parallel and return the smallest automaton."public static final StringSYMBOLIC_SE20_BKS10_DESCRIPTION"Translate the formula to a deterministic parity automaton by combining the LTL-to-DRA translation of [SE20] with DRAxDSA-to-DPA result of [BKS10]. This translation has an _symbolic_ implementation and is provided for testing purposes through this interface. In order to benefit from the symbolic implementation users _must_ use the \'SymbolicAutomaton\'-interface." -
owl.translations.LtlTranslationRepository.LtlToDraTranslation Modifier and Type Constant Field Value public static final StringEKS16_DESCRIPTION"Translate the formula to a deterministic (generalised) Rabin automaton by guessing and checking the set of greatest fixed-point operators, i.e. G, R, and W, that is satisfied by almost all suffixes of the word read by the automaton. This construction is also known as the original \'Rabinizer\'-construction [EKS16] and used to be available through the \'--asymmetric\' option."public static final StringEKS20_DESCRIPTION"Translate the formula to a deterministic (generalised) Rabin automaton by guessing and checking the set of greatest fixed-point operators, i.e. G, R, and W, that is satisfied by almost all suffixes of the word read by the automaton and the set of least fixed-point operators, i.e. F, M, and U, that is satisfied by infinitely many suffixes of the word read by the automaton. This construction has been initially proposed in [EKS18] and has been described in more detail and with optimisations in [S19]. The preferred reference to cite is the journal article [EKS20]. The translation used to be available through the \'--symmetric\' option."public static final StringSE20_DESCRIPTION"Translate the formula to a deterministic (generalised) Rabin automaton by rewriting the formula into the \u0394\u2082-normalform using the procedure of [SE20] and then by using the constructions for \'simple\' LTL fragments from [SE20, S19]."public static final StringSMALLEST_AUTOMATON_DESCRIPTION"Run all available D(G)RA-translations with all optimisations turned on in parallel and return the smallest automaton." -
owl.translations.LtlTranslationRepository.LtlToLdbaTranslation Modifier and Type Constant Field Value public static final StringEKS20_DESCRIPTION"Translate the formula to a limit-deterministic (generalised) B\u00fcchi automaton by guessing and checking the set of greatest fixed-point operators, i.e. G, R, and W, that is satisfied by almost all suffixes of the word read by the automaton and the set of least fixed-point operators, i.e. F, M, and U, that is satisfied by infinitely many suffixes of the word read by the automaton. This construction has been initially proposed in [EKS18] and has been described in more detail and with optimisations in [S19]. The preferred reference to cite is the journal article [EKS20]. The translation used to be available through the \'--symmetric\' option."public static final StringSEJK16_DESCRIPTION"Translate the formula to a limit-deterministic (generalised) B\u00fcchi automaton by guessing and checking the set of greatest fixed-point operators, i.e. G, R, and W, that is satisfied by almost all suffixes of the word read by the automaton. The construction is an optimised version of the construction appearing in [SEJK16] and used to be available through the \'--asymmetric\' option."public static final StringSMALLEST_AUTOMATON_DESCRIPTION"Run all available LD(G)BA-translations in parallel and return the smallest automaton." -
owl.translations.LtlTranslationRepository.LtlToNbaTranslation Modifier and Type Constant Field Value public static final StringEKS20_DESCRIPTION"Translate the formula to a non-deterministic (generalised) B\u00fcchi automaton by guessing and checking the set of greatest fixed-point operators, i.e. G, R, and W, that is satisfied by almost all suffixes of the word read by the automaton and the set of least fixed-point operators, i.e. F, M, and U, that is satisfied by infinitely many suffixes of the word read by the automaton. This construction has been initially proposed in [EKS18] and has been described in more detail and with optimisations in [S19]. The preferred reference to cite is the journal article [EKS20]. The translation used to be available through the \'--symmetric\' option."
owl.util.*
-
owl.util.ArraysSupport Modifier and Type Constant Field Value public static final intMAX_ARRAY_LENGTH2147483639
picocli.*
-
picocli.CommandLine Modifier and Type Constant Field Value public static final StringVERSION"4.6.1" -
picocli.CommandLine.ExitCode Modifier and Type Constant Field Value public static final intOK0public static final intSOFTWARE1public static final intUSAGE2 -
picocli.CommandLine.Help Modifier and Type Constant Field Value protected static final StringDEFAULT_COMMAND_NAME"<main class>"protected static final StringDEFAULT_SEPARATOR"=" -
picocli.CommandLine.Help.Ansi.IStyle Modifier and Type Constant Field Value public static final StringCSI"\u001b[" -
picocli.CommandLine.Model.CommandSpec Modifier and Type Constant Field Value public static final StringDEFAULT_COMMAND_NAME"<main class>" -
picocli.CommandLine.Model.OptionSpec Modifier and Type Constant Field Value public static final StringDEFAULT_FALLBACK_VALUE"" -
picocli.CommandLine.Model.UsageMessageSpec Modifier and Type Constant Field Value public static final intDEFAULT_USAGE_WIDTH80public static final StringSECTION_KEY_AT_FILE_PARAMETER"atFileParameterList"public static final StringSECTION_KEY_COMMAND_LIST"commandList"public static final StringSECTION_KEY_COMMAND_LIST_HEADING"commandListHeading"public static final StringSECTION_KEY_DESCRIPTION"description"public static final StringSECTION_KEY_DESCRIPTION_HEADING"descriptionHeading"public static final StringSECTION_KEY_END_OF_OPTIONS"endOfOptionsList"public static final StringSECTION_KEY_EXIT_CODE_LIST"exitCodeList"public static final StringSECTION_KEY_EXIT_CODE_LIST_HEADING"exitCodeListHeading"public static final StringSECTION_KEY_FOOTER"footer"public static final StringSECTION_KEY_FOOTER_HEADING"footerHeading"public static final StringSECTION_KEY_HEADER"header"public static final StringSECTION_KEY_HEADER_HEADING"headerHeading"public static final StringSECTION_KEY_OPTION_LIST"optionList"public static final StringSECTION_KEY_OPTION_LIST_HEADING"optionListHeading"public static final StringSECTION_KEY_PARAMETER_LIST"parameterList"public static final StringSECTION_KEY_PARAMETER_LIST_HEADING"parameterListHeading"public static final StringSECTION_KEY_SYNOPSIS"synopsis"public static final StringSECTION_KEY_SYNOPSIS_HEADING"synopsisHeading" -
picocli.CommandLine.Option Modifier and Type Constant Field Value public static final StringNULL_VALUE"_NULL_" -
picocli.CommandLine.Parameters Modifier and Type Constant Field Value public static final StringNULL_VALUE"_NULL_"