Code

Uclid5-based LF Verifier#1271

Code

Merged

lhstrh merged 189 commits intomasterlf-lang/lingua-franca:masterfrom verifierlf-lang/lingua-franca:verifierCopy head branch name to clipboardJul 25, 2023

+8,139-103

Commits

Commits on Nov 22, 2022

• Begin the Java port of the UclidGenerator

  lsk567

  committed
  f03bf86

• Do some more porting

  lsk567

  committed
  905bbcc

• Finish generating traces

  lsk567

  committed
  e8fe270

• Minor fixes

  lsk567

  committed
  b09633f

• Start to generate reaction and state variable declarations

  lsk567

  committed
  9a73349

• Ensure that when building the reaction instance graph, nodes are not being removed.

  lsk567

  committed
  7b31537

• Generate state variables and triggers

  lsk567

  committed
  f3d9cc8

• Generate up to reactor semantics

  lsk567

  committed
  21d1718

• Generate runner script and refactor a few things. TODO: Triggers, reactions, and DSL-related things.

  lsk567

  committed
  c5bc411

• Uclid bug fixes

  lsk567

  committed
  d704e51

• Start to generate reactions and triggers

  lsk567

  committed
  7e1a726

• Continue generating reactions

  lsk567

  committed
  f3a54c6

• Start populating state variables and triggers

  lsk567

  committed
  5d8d9a4

• Keep generating lists

  lsk567

  committed
  c2bccb5

• Remove dead code

  lsk567

  committed
  7bba94a

• Finish generating actions

  lsk567

  committed
  1e8e401

• Deprecate reaction instance graph

  lsk567

  committed
  49d11e3

• Generate connections

  lsk567

  committed
  646ba72

• Bug fix

  lsk567

  committed
  13db2db

• Start a C subset target

  lsk567

  committed
  60c5700

• Remove the super.doGenerate() call.

  lsk567

  committed
  8baa668

• Remove the new target. Invoke the uclid generator when @Property is in use.

  lsk567

  committed
  faa5203

• Add an instance class for state variables

  lsk567

  committed
  7d79196

• Add Antlr4 to the gradle project

  lsk567

  committed
  f194a01

• Move Antlr grammar

  lsk567

  committed
  7c9274c

• Fix Antlr generated file location, start MTL transpiler

  lsk567

  committed
  301ed16

• Start to generate properties based on property attributes

  lsk567

  committed
  52040d0

• Use the MTLParser to generate parse trees

  lsk567

  committed
  21efab8

• Update syntax to include expressions

  lsk567

  committed
  38a31ff

• Start to transpile MTL using a visitor

  lsk567

  committed
  47ab696

• Keep working on transpiling

  lsk567

  committed
  511d3a8

• Transpile Until

  lsk567

  committed
  59b23f5

• Refactor timing related visitor helper functions

  lsk567

  committed
  66edad4

• Checkpoint. Transpile up to Expr.

  lsk567

  committed
  666e70f

• Transpile up to Quotient

  lsk567

  committed
  6e2a180

• Generate properties

  lsk567

  committed
  a531123

• Add C grammar and AST visitors

  lsk567

  committed
  ba15655

• Integrate C parser with the UclidGenerator

  lsk567

  committed
  4f8c27e

• Start generating uclid axioms. Generate up to TriggerValue.

  lsk567

  committed
  6bedfcc

• Lift more AST nodes to Uclid

  lsk567

  committed
  aeb9867

• Generate more Uclid axioms from C

  lsk567

  committed
  4fc7147

• Removed the relaxation fragment in the connection axiom. Add dedicated axioms that resets an input port to default value. Reactions only reset state variables and output ports.

  lsk567

  committed
  be621d5

• Bug fixes

  lsk567

  committed
  d9e2b4b

• Fix bugs and generate more axioms

  lsk567

  committed
  f29cf78

• Fix bugs on setting a port while scheduling an action, reset unused ports, and maintain unused state variables

  lsk567

  committed
  60df7ce

• Prune dead code, attach value to action

  lsk567

  committed
  965eca5

• Add CAst utils

  lsk567

  committed
  712efb9

• Fix tag_schedule, action one-to-one correspondence, and startup axioms

  lsk567

  committed
  f5915f3

• Add a (temporary) fix for variable precedence.

  lsk567

  committed
  4d20a64

• Add precedence visitor

  lsk567

  committed
  b64e3f4

• Update schedule action mechanism and variable precedence. Verifier v0.1.

  lsk567

  committed
  5a1a2b3

• Update benchmarks

  lsk567

  committed
  4bcb0cf

• Update comments

  lsk567

  committed
  a4d373e

• Add comments

  lsk567

  committed
  70511bf

• Minor update

  lsk567

  committed
  07a8c8d

• Generate verification models in a "model-gen" directory.

  lsk567

  committed
  f53d45d

• Use arrays instead of tuples to represent traces

  lsk567

  committed
  9845797

Commits on Dec 1, 2022

• Start to work on a state space explorer

  lsk567

  committed
  cb667aa

• Detect back loop in the state space diagram.

  lsk567

  committed
  80f7c09

Commits on Dec 2, 2022

• Add trace padding to account for partial trace

  lsk567

  committed
  b69209e

Commits on Dec 3, 2022

• Add UclidRunner that runs uclid models and parses CEX traces

  lsk567

  committed
  5baf0c7

Commits on Dec 5, 2022

• Start to work on the logical time based semantics.

  lsk567

  committed
  66da9c7

• More robust CEX parsing, fix an axiom bug related to END_TRACE.

  lsk567

  committed
  0c8ab2d

Commits on Dec 7, 2022

• Support timers

  lsk567

  committed
  8d9d091

Commits on Dec 14, 2022

• Update CT estimation, clean up println.

  lsk567

  committed
  57eda6f

• Refactor uclid, C ast, and state space into an analyses package.

  lsk567

  committed
  9423212

Commits on Dec 15, 2022

• Make loop detection more efficient

  lsk567

  committed
  72eb050

Commits on Dec 16, 2022

• Fix loop period, generate dot file from state space diagram.

  lsk567

  committed
  65560ab

Commits on Dec 17, 2022

• Update dot formatting

  lsk567

  committed
  4f5e416

Commits on Dec 28, 2022

• Add an option to generate compact state space diagrams

  lsk567

  committed
  b2fddc1

• Support negative numbers in C code

  lsk567

  committed
  cd7fda8

• Address the case when the state space diagram only has one node.

  lsk567

  committed
  83a4f48

• Update comments

  lsk567

  committed
  03ae166

• Differentiate how tags increment for actions and connections

  lsk567

  committed
  0a55dda

Commits on Jan 3, 2023

• Fix CT calculation, fix state space node insertion, support manually specified CT, support the --no-verify flag

  lsk567

  committed
  185f6f2

Commits on Jan 4, 2023

• Compare timestamps only to match MTL semantics.

  lsk567

  committed
  a1b27ea

Commits on Jan 12, 2023

• Ensure uniqueness of reactions and events during state space exploration

  lsk567

  committed
  cf69123

Commits on Feb 4, 2023

• Fix the FOL encoding of Globally.

  lsk567

  committed
  1794136

Commits on Feb 5, 2023

• Support lf_schedule_int()

  lsk567

  committed
  78baf93

Commits on Feb 7, 2023

• Add a uniqueness axiom, update CEX parser to support let bindings

  lsk567

  committed
  344c34a

• Add happen-before relations based on priorities, fix C AST generation.

  lsk567

  committed
  2b99656

Commits on Feb 18, 2023

• Add preliminary github action workflow

  lsk567

  committed
  f5e12da

• Merge branch 'master' into verifier

  lsk567

  committed
  e16592c

• Try to trigger CI

  lsk567

  committed
  ff47ed0

• Try again

  lsk567

  committed
  fdff6b5

Commits on Feb 19, 2023

• Debug workflows

  lsk567

  committed
  5a13516

• Setup ssh after installing sbt

  lsk567

  committed
  a232244

• Attempt to fix a directory issue

  lsk567

  committed
  22ec9ff

Commits on Feb 21, 2023

• Add an 'expect' field to @Property

  lsk567

  committed
  d208f4c

• Update CI to run the test script

  lsk567

  committed
  6b760c8

• Relocate the CI script.

  lsk567

  committed
  d23906f

• Specify version

  lsk567

  committed
  ac43a76

• Fix version

  lsk567

  committed
  e77e60c

• Fix typo

  lsk567

  committed
  489a563

• Relocate the yml file.

  lsk567

  committed
  11d985f

• Emphasize local workflow

  lsk567

  committed
  c02b3b1

• Remove caching

  lsk567

  committed
  5c725d8

• Fix branch name

  lsk567

  committed
  276811b

• Fetch history

  lsk567

  committed
  662867e

• Remove SSH and update CI

  lsk567

  committed
  6ad8f4b

• Fix Globally

  lsk567

  committed
  4a38b8f

Commits on Mar 2, 2023

• Merge branch 'master' into verifier

  lhstrh

  authored
  407a787

Commits on Mar 3, 2023

• Merge branch 'master' into verifier

  lsk567

  committed
  c8df9d1

• Let the event queue sort based on both tags and trigger names

  lsk567

  committed
  17828a2

• Prune dead code

  lsk567

  committed
  22a7b11

Commits on Mar 23, 2023

• Temporarily remove the author tag for Shaokai.

  lsk567

  committed
  46e84c6

• Minor MTL grammar update

  lsk567

  committed
  8ba0f96

• Minor update

  lsk567

  committed
  7802314

• Merge branch 'master' into verifier

  lsk567

  committed
  db8c044

Commits on Mar 24, 2023

• Make --no-verify work again

  lsk567

  committed
  7672fb2

• Remove unused lib

  lsk567

  committed
  c079327

• Revert "Minor MTL grammar update"

  Show description for 95e8743
  lsk567

  committed
  95e8743

Commits on Jun 4, 2023

• Only extend horizon when it becomes larger

  lsk567

  committed
  40b9ce2

• Merge branch 'master' into verifier

  lsk567

  committed
  4c0bb09

• Remove top level org.lflang

  lsk567

  committed
  a36c991

• Update gradle and relocate analyses and dsl folders

  lsk567

  committed
  8b20b53

Commits on Jun 5, 2023

• Update CI and spotless

  lsk567

  committed
  2241047

Commits on Jun 7, 2023

• Fix git merge issues

  lsk567

  committed
  00172c7

• Add warnings and check dependencies

  lsk567

  committed
  a297808

• Merge branch 'master' into verifier

  lsk567

  committed
  a0634ee

• Update CI

  lsk567

  committed
  8525fb0

• Update CI

  lsk567

  committed
  9cc84c3

• Update CI

  lsk567

  committed
  aa7ed02

• Format Java files.

  petervdonovan

  committed
  622b496

• Merge branch 'master' into verifier

  petervdonovan

  committed
  95ca972

Commits on Jun 18, 2023

• use the antlr gradle plugin

  cmnrd

  committed
  3d0670b

• Merge branch 'master' into verifier

  lhstrh

  authored
  3f9cc88

• Update gradle.properties

  lhstrh

  authored
  fd9a94c

Commits on Jun 19, 2023

• don't format generated java files

  cmnrd

  committed
  fff61cf

• fix kotlin antlr dependencies

  cmnrd

  committed
  5612775

• clean up source sets

  cmnrd

  committed
  2d9d653

Commits on Jun 20, 2023

• Merge branch 'master' into verifier

  lsk567

  authored
  34837e5

Commits on Jun 21, 2023

• Merge branch 'master' into verifier

  lsk567

  authored
  93e021b

Commits on Jun 22, 2023

• Merge branch 'master' into verifier

  lsk567

  authored
  80b7983

• Apply suggestions from @petervdonovan

  Show description for be77b45
  

  lsk567

  and

  petervdonovan

  authored
  be77b45

• Apply more suggestions from @petervdonovan

  lsk567

  committed
  d4ed4d5

• Apply spotless

  lsk567

  committed
  6d92a9e

• Merge branch 'master' into verifier

  lsk567

  committed
  d0bd104

• Apply spotless

  lsk567

  committed
  02b2bc6

• Relocate doc comments

  lsk567

  committed
  77b5aa1

• Remove some inconsistent comments

  lsk567

  committed
  baa5061

Commits on Jun 23, 2023

• Throw exceptions instead of printf

  lsk567

  committed
  df25bc0

• Apply suggestions from @petervdonovan

  lsk567

  committed
  b1308b0

• Do not check models by default, based on suggestions from @lhstrh

  lsk567

  committed
  a859a66

Commits on Jun 27, 2023

• Merge branch 'master' into verifier

  lsk567

  authored
  8ac1d04

Commits on Jun 30, 2023

• Merge branch 'master' into verifier

  lsk567

  authored
  b37b09d

• Factor out createMainInstantiation()

  lsk567

  committed
  ec0198c

• Factor generateTriggersAndReactions() into multiple smaller functions. Change tactic to an enum.

  lsk567

  committed
  f7d94f5

• Separate public from private variables

  lsk567

  committed
  f422a2a

• Improve pattern matching and apply spotless

  lsk567

  committed
  877ce36

Commits on Jul 1, 2023

• Merge branch 'master' into verifier

  lsk567

  authored
  52288a4

• Use more getters and setters, and mark certain variables final

  lsk567

  committed
  b1d35c0

• Remove sneakyThrow and apply spotless

  lsk567

  committed
  2e687e6

• Report warnings using messageReporter

  lsk567

  committed
  7c74e08

• Apply more suggestions from @petervdonovan

  lsk567

  committed
  0256af6

Commits on Jul 2, 2023

• Merge branch 'master' into verifier

  lsk567

  authored
  41b8b7d

Commits on Jul 3, 2023

• Merge branch 'master' into verifier

  lsk567

  authored
  be3ca98

Commits on Jul 4, 2023

• Merge branch 'master' into verifier

  lsk567

  authored
  01d7ddd

• Throw error when looking up named instances

  lsk567

  committed
  b4540ba

• Handle the equals() issue

  lsk567

  committed
  5043e30

• Prune unused code

  lsk567

  committed
  55583e1

Commits on Jul 5, 2023

• Merge branch 'master' into verifier

  lsk567

  authored
  e1556ea

• Apply suggestions from @lhstrh

  Show description for 9bb39cf
  

  lsk567

  and

  lhstrh

  authored
  9bb39cf

• Apply suggestions from @lhstrh

  lsk567

  committed
  9b5a6f8

• Fix typo

  lsk567

  committed
  eeedef7

• Remove the unused global variable

  lsk567

  committed
  6a1109e

Commits on Jul 8, 2023

• Fix get macro, SendToDownstream, and Correspondence axioms

  lsk567

  committed
  202c15c

• Use END_TRACE in a few more places since it is the default

  lsk567

  committed
  55435bd

Commits on Jul 10, 2023

• Merge branch 'master' into verifier

  lsk567

  committed
  bbf27ac

• Rename workflow

  lsk567

  committed
  a9d44ff

• Apply spotless

  lsk567

  committed
  233a741

Commits on Jul 11, 2023

• Merge branch 'master' into verifier

  lsk567

  authored
  119e046

Commits on Jul 12, 2023

• Add verifier tests for CI

  lsk567

  committed
  97e2897

• Apply spotless

  lsk567

  committed
  e588226

• Merge branch 'master' into verifier

  lsk567

  authored
  11b423e

• rename ping pong test to make the name unique

  cmnrd

  committed
  197c323

• add the verifier test category

  cmnrd

  committed
  00c04f7

• add verifier test class

  cmnrd

  committed
  4b83bcf

• exclude the verifier tests from zephyr and multithreaded

  cmnrd

  committed
  4db4404

• update CI

  cmnrd

  committed
  c9f80aa

• ensure correct directory

  cmnrd

  committed
  2747157

• Output error message when dependencies are not installed.

  lsk567

  committed
  d07e029

• actually ensure correct directory

  cmnrd

  committed
  06a8944

Commits on Jul 13, 2023

• bring workflow up to standard and add debug info

  cmnrd

  committed
  4696ee0

• Fix the assertion error.

  lsk567

  committed
  ad4daeb

Commits on Jul 14, 2023

• Adjust platform and test level

  lsk567

  committed
  2e7cfb0

Commits on Jul 18, 2023

• Update core/src/main/java/org/lflang/generator/LFGenerator.java

  lhstrh

  authored
  d87763f

Commits on Jul 19, 2023

• Merge branch 'master' into verifier

  lsk567

  authored
  5a13524

• Apply spotless

  lsk567

  committed
  35f0887