{"id":"W2401576199","doi":"10.1145/2896982.2896990","title":"Representing hierarchical state machine models in SMT-LIB","year":2016,"lang":"en","type":"article","venue":"","topic":"Formal Methods in Verification","field":"Computer Science","cited_by":2,"is_retracted":false,"has_abstract":true,"ca_institutions":"University of Waterloo","funders":"","keywords":"Computer science; Semantics (computer science); Syntax; Hierarchy; Programming language; Finite-state machine; Representation (politics); State (computer science); Exploit; Variety (cybernetics); Abstract syntax; Theoretical computer science; Artificial intelligence","routes":{"ca_aff":true,"ca_fund":false,"ca_venue":false,"about_ca":false,"invisible_to_affiliation_only":false},"retraction":null,"screen":null,"direct_labels":[],"prediction":{"model_version":"codex-gemma-dda1882f352a","candidate_categories":[],"consensus_categories":[],"category_scores_codex":[0.0008729663,0.00007358131,0.00009198342,0.0001095948,0.00003269613,0.0000491687,0.0006415508,0.00003033172,0.00002029002],"category_scores_gemma":[0.0001556163,0.00004683016,0.00002635553,0.0002660119,0.00003714583,0.0009787621,0.0003265504,0.0000943165,0.00004815471],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.00003485285,"about_ca_system_score_gemma":0.00002296922,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.00006657154,"about_ca_topic_score_gemma":0.00001373163,"domain_scores_codex":[0.9988392,0.0001523696,0.0002440807,0.0003247106,0.0001954895,0.0002441366],"domain_scores_gemma":[0.9991266,0.0001338052,0.00004909856,0.0006042224,0.00002759049,0.00005869141],"domain_codex":null,"domain_gemma":null,"domain_candidate":null,"domain_consensus":null,"study_design_codex":"theoretical_or_conceptual","study_design_gemma":"simulation_or_modeling","study_design_scores_codex":[0.000007884742,0.00003209639,0.001492862,0.000004198758,0.000002464926,0.000006580978,0.0002976364,0.0003969014,0.003566433,0.5833391,0.000074229,0.4107796],"study_design_scores_gemma":[0.0002485104,0.00001759939,0.004079701,0.00001631151,3.572468e-7,0.000006108656,0.000001993871,0.7952785,0.00817688,0.1916011,0.0004677947,0.0001051576],"study_design_candidate":"simulation_or_modeling","study_design_consensus":null,"genre_codex":"methods","genre_gemma":"methods","genre_scores_codex":[0.02740213,0.00001663943,0.9570543,0.001211411,0.0001287508,0.00008688802,7.670876e-7,0.000149128,0.01395003],"genre_scores_gemma":[0.3862862,0.00001161775,0.6121963,0.0001001151,0.00001222394,0.0000084042,1.882404e-7,0.000004501373,0.001380432],"genre_candidate":"methods","genre_consensus":"methods","teacher_disagreement_score":0.7948816,"threshold_uncertainty_score":0.1909679,"prediction_status":"machine_predicted_unvalidated"},"machine_scores":{"provisional":true,"baseline":true,"maturity_gate_passed":false,"score_opus":0.04290827532304629,"score_gpt":0.3017696438197035,"score_spread":0.2588613684966572,"validation_status":"score_only:v0-immature-baseline","note":"Baseline scores from an immature model (maturity gate not passed). Scores rank; they never assert a category."}}