<commit_before>#include <config.h>
#include <ltsmin-tl.h>
#include <runtime.h>
#include <dynamic-array.h>
#include <ltsmin-grammar.h>
#include <ltsmin-parse-env.h>
#include <ltsmin-lexer.h>

/******************************************************************
 * Note: some of these functions leak memory of type ltsmin_expr_t
 *****************************************************************/

/* LTL:
 *     <NAME>, <NAME> and <NAME>,
 *     Model Checking,
 *     MIT Press,1999
 *
 * Nonstandard connectives:
 * (Until)      p U q = F q | (p W q)
 * (Release)    p R q = q W (p & q)
 * (Release)    p R q = ! (!p U !q) (dual of until)
 * (Weak Until) p W q = q R (q | p)
 * (Weak Until) p W q = (p U q) | G p
 * (Strong Release) p M q = ! (!p W !q) (dual of weak until)
 *
 * Operator percendence
 *  HIGH
 *     ==, <=, >=, != (state label expression)
 *     !
 *     G, F, X
 *     &
 *     |
 *     ^ (XOR)
 *     <-> (EQUIV)
 *     -> (IMPLY)
 *     U, R
 *  LOW
 */

/* Parser Priorities:
 * HIGH
 *     binary priority 1          : ==, !=, etc
 *     prefix priority 2          : !
 *     prefix priority 3          : G,F,X
 *     binary priority 4          : &
 *     binary priority 5          : |
 *     binary priority 6          : <->
 *     binary priority 7          : <->
 *     binary priority 8          : U,R
 * LOW
 */
ltsmin_expr_t ltl_parse_file(lts_type_t ltstype,const char *file){
    FILE *in=fopen( file, "r" );
    if (!in) Fatal(1, error, "unable to open file: %s", file);
    ltsmin_parse_env_t env=LTSminParseEnvCreate();
    int N;
    N=lts_type_get_state_length(ltstype);
    for(int i=0;i<N;i++){
        char*name=lts_type_get_state_name(ltstype,i);
        if (name) LTSminStateVarIndex(env,name);
    }
    N=lts_type_get_state_label_count(ltstype);
    for(int i=0;i<N;i++){
        char*name=lts_type_get_state_label_name(ltstype,i);
        // consider state label an state variable
        if (name) LTSminStateVarIndex(env,name);
    }
    N=lts_type_get_edge_label_count(ltstype);
    for(int i=0;i<N;i++){
        char*name=lts_type_get_edge_label_name(ltstype,i);
        if (name) LTSminEdgeVarIndex(env,name);
    }

    LTSminConstant      (env, CTL_FALSE,        "false");
    LTSminConstant      (env, CTL_TRUE,         "true");

    LTSminBinaryOperator(env, LTL_EQ,           "==", 1);
    LTSminPrefixOperator(env, LTL_NOT,          "!",  2);

    LTSminPrefixOperator(env, LTL_GLOBALLY,     "[]", 3);
    LTSminPrefixOperator(env, LTL_FUTURE,       "<>", 3);
    LTSminPrefixOperator(env, LTL_NEXT,         "X",  3);

    LTSminBinaryOperator(env, LTL_AND,          "&",  4);
    LTSminBinaryOperator(env, LTL_OR,           "|",  5);

    LTSminBinaryOperator(env, LTL_EQUIV,        "<->",6);
    LTSminBinaryOperator(env, LTL_IMPLY,        "->", 7);

    LTSminBinaryOperator(env, LTL_UNTIL,        "U",  8);
    //LTSminBinaryOperator(env, LTL_WEAK_UNTIL,   "W",  8); // not supported by ltl2ba
    LTSminBinaryOperator(env, LTL_RELEASE,      "R",  8);

    ltsmin_parse_stream(TOKEN_EXPR,env,stream_input(in));
    ltsmin_expr_t expr=env->expr;<commit_msg>Align LTL syntax with SPIN's and DiVinE's<commit_after>#include <config.h>
#include <ltsmin-tl.h>
#include <runtime.h>
#include <dynamic-array.h>
#include <ltsmin-grammar.h>
#include <ltsmin-parse-env.h>
#include <ltsmin-lexer.h>

/******************************************************************
 * Note: some of these functions leak memory of type ltsmin_expr_t
 *****************************************************************/

/* LTL:
 *     <NAME>, <NAME> and <NAME>,
 *     Model Checking,
 *     MIT Press,1999
 *
 * Nonstandard connectives:
 * (Until)      p U q = F q | (p W q)
 * (Release)    p R q = q W (p & q)
 * (Release)    p R q = ! (!p U !q) (dual of until)
 * (Weak Until) p W q = q R (q | p)
 * (Weak Until) p W q = (p U q) | G p
 * (Strong Release) p M q = ! (!p W !q) (dual of weak until)
 *
 * Operator percendence
 *  HIGH
 *     ==, <=, >=, != (state label expression)
 *     !
 *     G, F, X
 *     &
 *     |
 *     ^ (XOR)
 *     <-> (EQUIV)
 *     -> (IMPLY)
 *     U, R
 *  LOW
 */

/* Parser Priorities:
 * HIGH
 *     binary priority 1          : ==, !=, etc
 *     prefix priority 2          : !
 *     prefix priority 3          : G,F,X
 *     binary priority 4          : &
 *     binary priority 5          : |
 *     binary priority 6          : <->
 *     binary priority 7          : <->
 *     binary priority 8          : U,R
 * LOW
 */
ltsmin_expr_t ltl_parse_file(lts_type_t ltstype,const char *file){
    FILE *in=fopen( file, "r" );
    if (!in) Fatal(1, error, "unable to open file: %s", file);
    ltsmin_parse_env_t env=LTSminParseEnvCreate();
    int N;
    N=lts_type_get_state_length(ltstype);
    for(int i=0;i<N;i++){
        char*name=lts_type_get_state_name(ltstype,i);
        if (name) LTSminStateVarIndex(env,name);
    }
    N=lts_type_get_state_label_count(ltstype);
    for(int i=0;i<N;i++){
        char*name=lts_type_get_state_label_name(ltstype,i);
        // consider state label an state variable
        if (name) LTSminStateVarIndex(env,name);
    }
    N=lts_type_get_edge_label_count(ltstype);
    for(int i=0;i<N;i++){
        char*name=lts_type_get_edge_label_name(ltstype,i);
        if (name) LTSminEdgeVarIndex(env,name);
    }

    LTSminConstant      (env, CTL_FALSE,        "false");
    LTSminConstant      (env, CTL_TRUE,         "true");

    LTSminBinaryOperator(env, LTL_EQ,           "==", 1);
    LTSminPrefixOperator(env, LTL_NOT,          "!",  2);

    LTSminPrefixOperator(env, LTL_GLOBALLY,     "[]", 3);
    LTSminPrefixOperator(env, LTL_FUTURE,       "<>", 3);
    LTSminPrefixOperator(env, LTL_NEXT,         "X",  3);

    LTSminBinaryOperator(env, LTL_AND,          "&&",  4);
    LTSminBinaryOperator(env, LTL_OR,           "||",  5);

    LTSminBinaryOperator(env, LTL_EQUIV,        "<->",6);
    LTSminBinaryOperator(env, LTL_IMPLY,        "->", 7);

    LTSminBinaryOperator(env, LTL_UNTIL,        "U",  8);
    //LTSminBinaryOperator(env, LTL_WEAK_UNTIL,   "W",  8); // not supported by ltl2ba
    LTSminBinaryOperator(env, LTL_RELEASE,      "R",  8);

    ltsmin_parse_stream(TOKEN_EXPR,env,stream_input(in));
    ltsmin_expr_t expr=env->expr;
{'fraction_non_alphanumeric': 0.18524433088470138, 'fraction_numerical': 0.009262216544235069, 'mean_word_length': 2.597357840321654, 'pattern_counts': {'":': 0, '<': 41, '<?xml version=': 0, '>': 41, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '2306316', 'n_tokens_mistral': 2406, 'n_tokens_neox': 2331, 'n_words': 493}