s14h
/
prism-accumulation
1
0
Fork 0
Code Releases Activity
3018 Commits
5 Branches
0 Tags
31 MiB
Tree: cf16b66849
Branches Tags
${ item.name }
Create tag ${ searchTerm }
Create branch ${ searchTerm }
from 'cf16b66849'
${ noResults }
Commit Graph

344 Commits (cf16b668491b97088dcbf56e8b8fc7fc2accd424)

Author SHA1 Message Date
Joachim Klein ba6c74270f Property: handle missing constant in search for right // RESULT line
10 years ago
Joachim Klein 52dc54df5b ConstantList: methods for removing a constant definition
10 years ago
Joachim Klein 7cd20911e9 ast.Property: tidy comment
10 years ago
Joachim Klein 53036fa388 Property.checkAgainstExpectedResultString: Integer results in exact mode
10 years ago
Joachim Klein e1105ab74a Property.checkAgainstExpectedResultString: handle complex expressions
10 years ago
Joachim Klein 2c8f5427b5 Expression: add evaluateExact methods
10 years ago
Joachim Klein d6e222a4e1 RESULT handling for Property: Invert order for picking RESULT
10 years ago
Joachim Klein aa3ec454a8 ConstantList: add constructor from Values object
10 years ago
Joachim Klein 69211a1c35 ConstantList: move initialisation to the variable definitions
10 years ago
Dave Parker ec0428f084 Update parser files to version 6.0 of JavaCC.
10 years ago
Joachim Klein a81aec5199 Simplify: add handling for ExpressionITE (fixes a PTA bug) [by Linda Leuschner]
10 years ago
Joachim Klein e165b9f9a6 refactor testing against PrismNotSupportedException
10 years ago
Joachim Klein 5cfe76d82a visitor.ReplaceLabels: for replacing labels in an expression
10 years ago
Dave Parker e2074832df Switch from ModuleFile to ModelInfo in Values object.
10 years ago
Dave Parker efbeda6faf Switch from ModuleFile to ModelInfo in State object.
10 years ago
Vojtech Forejt 2d8194398b Fixed a bug where the type of multi was not correctly determined if boolean arguments came before double arguments. Now we enforce doubles to be given first.
10 years ago
Vojtech Forejt efff3c629b Removing superfluous debugging output
10 years ago
Vojtech Forejt 563d0bd772 Added capability for testing Pareto curves (no tests added yet, and the Pareto curve generation itself is still buggy)
10 years ago
Joachim Klein ea537cc895 Expression.containsTemporalTimeBounds(): do not recurse into P/R/SS subformulas
10 years ago
Joachim Klein 366660dac4 parser.visitor.ExpressionTraverseNonNested: Helper for traversing Expressions without recursing into nested P/R/SS formulas
10 years ago
Dave Parker 4c13267ded Add test methods for special cases in ExpressionLabels.
10 years ago
Dave Parker d1468e2bd8 Fix recent changes to ExpressionFilter: lower case keywords got lost.
10 years ago
Dave Parker bf59b2c9f7 Fix bug from new ModelInfo stuff: shows up when PropertiesFile model info is null (e.g. from GUI).
10 years ago
Dave Parker dbac067052 Bugfix for last commit: filter op name got lost.
10 years ago
Dave Parker 0d4ea5b904 Simplify parsing of filter operators in ExpressionFilter. [from Steffen Marcker]
10 years ago
Dave Parker 4449ad4cd1 Further commenting in FilterOperator.
10 years ago
Dave Parker 04d348fabd Commenting in ExpressionFilter operators. [from Steffen Marcker]
10 years ago
Dave Parker 0f2bbbc7b6 Add some (syntactic) reward info to the ModelInfo interface and use this where possible in explicit model checking. Can now use ModulesFileModelGenerator for reward property model checking. Also push constant info from ModelGenerator up to ModelInfo.
10 years ago
Dave Parker 2fe6c5d762 Add basic variable info to ModelInfo interface.
11 years ago
Dave Parker 6e20db3f60 Comment typo
11 years ago
Dave Parker 388e8b5908 Add initial support to Prism API to load ModelGenerator objects + some associated changes in infrastructure + a test case.
11 years ago
Dave Parker 7ff1ffe2db Make ModulesFile implement new ModelInfo interface.
11 years ago
Dave Parker 9ce7e6441b Push containsUnboundedVariables methof from VarList up into ModulesFile.
11 years ago
Dave Parker f16da3762d Add missing file from last commit.
11 years ago
Dave Parker 17087eee26 Decompose semantics checks (into expressions, models, properties). This will facilitate later attempts to make model checking less tied to ModulesFile specifically, rather than other model sources.
11 years ago
Dave Parker 8775d3a993 Small fix in Expression static constructors to make return types more clearly specified. [from Steffen Marcker]
11 years ago
Dave Parker 87b50d7da2 Small change in ExpandPropRefsAndLabels: either properties list or lable list can be omitted (and is then ignored).
11 years ago
Dave Parker b1f83bfbf5 Small fix: slightly more efficient recursion in ExpandLabels and ExpandPropRefsAndLabels.
11 years ago
Joachim Klein 043c776914 Refactor ConvertForJltl2ba (fix regression due to custom equals/hashCode for ASTElements)
11 years ago
Dave Parker f95f76ab81 Bugfix in PRISM-to-Latex translation.
11 years ago
Dave Parker c373555f9c Refactoring multi-objective code: readying for allowing lists of objectives in strategy operator.
11 years ago
Dave Parker cec60108c2 Comment clarification.
11 years ago
Dave Parker d4c5fd4fd5 Remove accidental commits
11 years ago
Dave Parker ff05caf158 Code tidy.
11 years ago
Dave Parker ce6131636e Some refactoring of the RelOp and ModelType enums. [from Steffen Marcker]]
11 years ago
Dave Parker 7511a39939 Additional functionality in LTL parser test code.
11 years ago
Dave Parker 1097ecaaeb Add a second syntactic co-safe-ness check, which first converts to positive normal form.
11 years ago
Dave Parker 2c6fece3d9 Auto-format
11 years ago
Dave Parker f85e2cfa85 Remove some unnecessary exception throwing from functions in BooleanUtils.
11 years ago
Dave Parker f7e4b6f747 Comment typo
11 years ago