prism-accumulation

3682 Commits

5 Branches

0 Tags

31 MiB

Tree: bfbb00f54c

Commit Graph

Author	SHA1	Message	Date
Joachim Klein	4f0137933c	param / exact: Evaluate expressions exactly in various places (+tests) Expressions are now evaluated exactly in parametric / exact model checking mode for: - state updates - command guards - the if part of if-then-else expressions - reward guards - reward values - Boolean expressions in RESULTS in property files Add various test cases to check that it is now handled properly.	9 years ago
Joachim Klein	6c0294923e	Use exact evaluation of constant expressions in exact and parametric mode Using the infrastructure from the previous commit, we request exact evaluation of constants in exact and parametric model checking mode. Additionally, note where we deliberately choose non-exact evaluation mode. Add corresponding test cases.	9 years ago

Author

SHA1

Message

Date

Joachim Klein

4f0137933c

param / exact: Evaluate expressions exactly in various places (+tests)

Expressions are now evaluated exactly in parametric / exact model checking mode for:
 - state updates
 - command guards
 - the if part of if-then-else expressions
 - reward guards
 - reward values
 - Boolean expressions in RESULTS in property files

Add various test cases to check that it is now handled properly.

9 years ago

Joachim Klein

6c0294923e

Use exact evaluation of constant expressions in exact and parametric mode

Using the infrastructure from the previous commit, we request exact evaluation
of constants in exact and parametric model checking mode.

Additionally, note where we deliberately choose non-exact evaluation mode.

Add corresponding test cases.

9 years ago

1 Commits (bfbb00f54c2aa77e006fe4c7a5e6a031d0efa64c)