Code

iMC changes inside of storm-pars#640

Code

Draft

linusheck wants to merge 171 commits intomoves-rwth:mastermoves-rwth/storm:masterfrom linusheck:robustplalinusheck/storm:robustplaCopy head branch name to clipboard

+7,529-3,096

Commits

Commits on Feb 12, 2024

• Add Robust Parameter Lifting Algorithm

  glatteis

  committed
  e16f242

Commits on Feb 14, 2024

• Merge branch 'master' of github.com:moves-rwth/storm into robustpla

  glatteis

  committed
  0d0675c

Commits on Feb 19, 2024

• First version of horizon-bounded big-step and time-travelling

  glatteis

  committed
  b829776

• applyRowRobust optimization

  glatteis

  committed
  fd8acbe

Commits on Feb 21, 2024

• Revert changes in ValueIterationOperator.cpp

  glatteis

  committed
  7cae91c

Commits on Feb 23, 2024

• Add support for ill-defined regions

  glatteis

  committed
  0e06f0c

• Revert "Revert changes in ValueIterationOperator.cpp"

  Show description for f2571c3
  glatteis

  committed
  f2571c3

Commits on Feb 27, 2024

• WIP commit

  glatteis

  committed
  135619b

• Revert "Revert "Revert changes in ValueIterationOperator.cpp""

  Show description for 4b94de0
  glatteis

  committed
  4b94de0

Commits on Feb 29, 2024

• Best version of robust value iteration

  glatteis

  committed
  bee2544

Commits on Mar 4, 2024

• Fix: copy x here

  glatteis

  committed
  49e2860

Commits on Mar 11, 2024

• New RegionRefinementChecker and AnnotatedRegion (work in progress)

  tquatmann

  committed
  a9f25c2

Commits on Mar 12, 2024

• Almost works?

  glatteis

  committed
  5a97d3d

Commits on Mar 13, 2024

• towards compiling again and a simpler ValidatingSparseParameterLiftingModelChecker (work in progress)

  tquatmann

  committed
  28f51ac

Commits on Mar 15, 2024

• A lot of stuff, everywhere

  glatteis

  committed
  af044ee

• Format

  glatteis

  committed
  ac1d2f4

• WIP refactor of TimeTravelling.cpp (does not compile yet)

  glatteis

  committed
  d432df3

Commits on Mar 16, 2024

• towards compiling again and OrderBasedMonotonicityBackend (work in progress)

  tquatmann

  committed
  9c0ccc4

Commits on Mar 19, 2024

• Finally compiling again. Not tested yet.

  tquatmann

  committed
  105b9d9

Commits on Mar 20, 2024

• work on order-based monotonicity backend & various fixes

  tquatmann

  committed
  d3cee7f

• Fixed build with cln numbers

  tquatmann

  committed
  878fe6f

• refactor time-travelling

  glatteis

  committed
  b325ea3

Commits on Mar 21, 2024

• whoops

  glatteis

  committed
  5f75b2a

• Fixed build with cln numbers [Part 2]

  tquatmann

  committed
  23d92f8

• Fix cubicEquationZeroes code

  glatteis

  committed
  faa786d

• 3 fixes

  tquatmann

  committed
  b12e273

Commits on Mar 22, 2024

• Correct preprocessing for b-vectors with intervals in ValueIterationHelper.h

  glatteis

  committed
  bd610ac

• Merge branch 'master' of github.com:moves-rwth/storm into robustpla

  glatteis

  committed
  03c9f5d

• Optimize time-travelling

  glatteis

  committed
  26f31d6

Commits on Mar 25, 2024

• Fix non-const ASSERT statement that broke in release mode

  glatteis

  committed
  1595d86

Commits on Mar 27, 2024

• Find polynomial roots using SMT solver

  glatteis

  committed
  df78b3f

• bigstep rewrite

  glatteis

  committed
  8cb8882

Commits on Apr 2, 2024

• New BigStep algorithm uses DFS and BFS :)

  glatteis

  committed
  201ce51

• Cache polynomial multiplication, polynomial addition still slow

  glatteis

  committed
  1856ad3

• Still a couple of TODOs left, mainly the incredibly slow operations on RationalFunction, but new bigstep is working

  glatteis

  committed
  3407d5e

• Talk to the SMT solver a little better

  glatteis

  committed
  e6eed5c

• Fix updateTreeStates

  glatteis

  committed
  c3ace88

Commits on Apr 8, 2024

• Fix TimeTravellingTest to use strong bisim

  glatteis

  committed
  1ae3748

• Merge branch 'master' of github.com:moves-rwth/storm into robustpla

  glatteis

  committed
  3dd506a

• New method name for robust scheduler tracking helper

  glatteis

  committed
  f3d8edf

• Find roots with CARL as well

  glatteis

  committed
  601e2c7

Commits on Apr 10, 2024

• Make time-travelling work with only the annotations

  glatteis

  committed
  e230dbb

• Polished code

  tquatmann

  committed
  664474e

• Remove commented code

  tquatmann

  committed
  86b54c8

• Split MonotonicityAnnotation from AnnotatedRegion

  tquatmann

  committed
  b314bb8

• Interval arithmetic works but I still need to figure out how to do this efficiently

  glatteis

  committed
  f81753a

Commits on Apr 11, 2024

• implemented feedback by LH

  tquatmann

  committed
  4b37b5f

• clean-up of includes, silence warning concerning usage of class vs. sruct

  tquatmann

  committed
  8a148ac

Commits on Apr 12, 2024

• WIP: Rootfinding

  glatteis

  committed
  595a20a

Commits on Apr 17, 2024

• WIP: Interval Arithmetic

  glatteis

  committed
  3e02cce

Commits on Apr 24, 2024

• Mix derivative intervalling with rootfinding

  glatteis

  committed
  b0abc39

Commits on May 1, 2024

• Solve grid issue

  glatteis

  committed
  588d7d8

Commits on May 3, 2024

• Performance-related fixes

  glatteis

  committed
  82d0335

Commits on May 7, 2024

• Add round-robin and CLI stuff for region refinement

  glatteis

  committed
  00c436f

Commits on May 8, 2024

• Implement estimate-based splitting

  glatteis

  committed
  c8efba6

Commits on May 21, 2024

• Add --estimate-method CLI argument

  glatteis

  committed
  6686607

• Do not split on monotone parameters if mode is feasibility

  glatteis

  committed
  eb1e3b0

• Small fixes

  glatteis

  committed
  01ad349

• Merge branch 'region-refinement' of github.com:linusheck/storm into robustpla

  glatteis

  committed
  1038219

• Amend estimate based strategy to not request estimates if maxSplitDimensions is larger than number of variables

  glatteis

  committed
  7783ca5

• Merge branch 'region-refinement' of github.com:linusheck/storm into robustpla

  glatteis

  committed
  ed351d4

Commits on May 24, 2024

• WIP commit

  glatteis

  committed
  d2227f1

Commits on May 27, 2024

• WIP commit

  glatteis

  committed
  fc1fffb

• Add regions to GD

  glatteis

  committed
  d32f833

Commits on Jun 3, 2024

• WIP: Add minmaxdelta strategies

  glatteis

  committed
  be5e682

Commits on Jun 5, 2024

• Conservative extension of state-value-delta

  glatteis

  committed
  7de29ca

Commits on Jun 20, 2024

• WIP

  glatteis

  committed
  22b586a

Commits on Jun 26, 2024

• Fix bigstep bug

  glatteis

  committed
  f323c96

Commits on Jun 28, 2024

• Compute subgraph, including edges, in time travelling

  glatteis

  committed
  61f40f1

Commits on Jul 3, 2024

• Add IntervalEndComponentPreserver

  glatteis

  committed
  8f2281e

Commits on Jul 9, 2024

• Update src/storm-pars-cli/storm-pars.cpp

  Show description for 9f908be
  

  linusheck

  and

  tquatmann

  authored
  9f908be

• Update src/storm-pars-cli/storm-pars.cpp

  Show description for e17bcd4
  

  linusheck

  and

  tquatmann

  authored
  e17bcd4

• Update src/storm-pars/modelchecker/region/RegionRefinementChecker.cpp

  Show description for 0bfed3c
  

  linusheck

  and

  tquatmann

  authored
  0bfed3c

• Update src/storm-pars/modelchecker/region/SparseDtmcParameterLiftingModelChecker.cpp

  Show description for 361aabb
  

  linusheck

  and

  tquatmann

  authored
  361aabb

• Update src/storm-pars/modelchecker/region/RegionRefinementChecker.cpp

  Show description for b0d2a2a
  

  linusheck

  and

  tquatmann

  authored
  b0d2a2a

• Fix suggestions around RegionRefinementChecker loop

  glatteis

  committed
  dd31238

• PRINT_AND_LOG links now

  glatteis

  committed
  7ade3a1

• Fix second splitting loop

  glatteis

  committed
  9aa565c

• Fix format?

  glatteis

  committed
  2d6bf34

• Change region splitting strategy heuristic API

  glatteis

  committed
  26a689b

• Print default

  glatteis

  committed
  aee5f58

Commits on Jul 10, 2024

• Fix format?

  glatteis

  committed
  daaa039

Commits on Jul 16, 2024

• Complain if bigstep gets a non-probabilistic matrix

  glatteis

  committed
  21acd0b

• Fix compile

  glatteis

  committed
  502f8d8

• Merge branch 'robustpla' of github.com:glatteis/storm-private into robustpla

  glatteis

  committed
  cdb6a3b

Commits on Jul 18, 2024

• Fix weird Release GCC behavior

  glatteis

  committed
  1d68644

• Merge branch 'robustpla' of github.com:glatteis/storm-private into robustpla

  glatteis

  committed
  337ce74

• Fix Gmp number conversions and interval end component preserving

  glatteis

  committed
  9687630

Commits on Jul 23, 2024

• Fix incorrect check in ValueIterationOperator

  glatteis

  committed
  54aa476

Commits on Jul 25, 2024

• Fix result vector size

  glatteis

  committed
  d96aeba

• Fix the fix

  glatteis

  committed
  05725e9

• Fix bugs in interval component preserver, warm-start

  glatteis

  committed
  79d2f8e

Commits on Jul 26, 2024

• Fix assert

  glatteis

  committed
  9d34a8a

• Remove prints

  glatteis

  committed
  ac96a58

• Merge remote-tracking branch 'fork/region-refinement' into robustpla

  glatteis

  committed
  84cd4b6

• Merge branch 'robustpla' of github.com:glatteis/storm-private into robustpla

  glatteis

  committed
  ec85113

Commits on Aug 1, 2024

• Add --not-graph-preserving flag

  glatteis

  committed
  f739523

Commits on Aug 2, 2024

• Improve interval evaluation for non-factorizable polynomials

  glatteis

  committed
  f9a1c7e

• WIP: Add interval non-trivial MEC detection and elimination

  glatteis

  committed
  616f34e

• Merge branch 'not-graph-preserving' of github.com:linusheck/storm into robustpla

  glatteis

  committed
  1e6392a

• Does this fix the weird compile issue?

  glatteis

  committed
  3697673

• Remove some TODOs

  glatteis

  committed
  6061528

Commits on Aug 4, 2024

• Fix maze problem

  glatteis

  committed
  2e2f71f

• Fix bug in interval evaluation

  glatteis

  committed
  689cf57

Commits on Aug 5, 2024

• Preserve reward models in graph-preserving bisim

  glatteis

  committed
  2db851d

• Fix part of the tests :D

  glatteis

  committed
  80480af

• Fix target set bug, add tests for non-graph-preserving checker on graph-preserving regions

  glatteis

  committed
  ed19aa8

• Eliminate target, sink state from matrix

  glatteis

  committed
  5054a58

Commits on Aug 6, 2024

• Change behavior of MEC elimination, add test

  glatteis

  committed
  51ad42a

Commits on Aug 7, 2024

• Remove include

  glatteis

  committed
  f3dd68b

• fix some details, add some prints

  glatteis

  committed
  6901552

• Cache optimizations

  glatteis

  committed
  f00afcf

• add some optimizations that i hope actually make the code faster

  glatteis

  committed
  5a4c871

• fix derivatives

  glatteis

  committed
  74b6368

• remove couts

  glatteis

  committed
  4e58ef1

Commits on Aug 8, 2024

• Remove prints

  glatteis

  committed
  76dca2b

Commits on Aug 21, 2024

• Fix bug in bigstep

  glatteis

  committed
  c9f53a2

Commits on Aug 22, 2024

• aaahhh

  glatteis

  committed
  c7d12b3

Commits on Sep 13, 2024

• Small but important bigstep tweaks

  glatteis

  committed
  1cc4a06

• no couts

  glatteis

  committed
  30f0887

Commits on Sep 18, 2024

• Redirect eliminated in nontrivial MECs

  glatteis

  committed
  ad976d1

Commits on Sep 27, 2024

• Add discrete parameters

  glatteis

  committed
  8b0a840

• Do not split on fixed parameters

  glatteis

  committed
  7b1b8a3

Commits on Sep 30, 2024

• remove couts

  glatteis

  committed
  47dd410

Commits on Oct 4, 2024

• Fix parseVariableList

  glatteis

  committed
  f59aabc

Commits on Oct 8, 2024

• bigstep topological ordering

  glatteis

  committed
  482a6e8

Commits on Oct 9, 2024

• Simple special case

  glatteis

  committed
  bde6169

• Change pointing

  glatteis

  committed
  30f92a8

• more robust optimization

  glatteis

  committed
  ef4c0ca

• Fix estimate method

  glatteis

  committed
  ed18a69

• Fix estimate method

  glatteis

  committed
  2b47a71

• Revert "more robust optimization"

  Show description for 1fc089d
  glatteis

  committed
  1fc089d

• Revert "Change pointing"

  Show description for 6eb1701
  glatteis

  committed
  6eb1701

• Revert "Simple special case"

  Show description for 06a5434
  glatteis

  committed
  06a5434

Commits on Oct 11, 2024

• just trying something out...

  glatteis

  committed
  c94d846

• fix stateeliminator

  glatteis

  committed
  845de7b

Commits on Oct 12, 2024

• Fix estimate bug

  glatteis

  committed
  9878a51

Commits on Oct 28, 2024

• Merge branch 'master' of github.com:moves-rwth/storm into robustpla

  glatteis

  committed
  7eb0faa

Commits on Oct 29, 2024

• Header fixes

  glatteis

  committed
  8a144f6

• setup Topological MinMax equation solver so I can eventually port it to iMCs

  glatteis

  committed
  02cc238

Commits on Nov 1, 2024

• WIP on feasibility

  glatteis

  committed
  cad7131

• Merge branch 'master' of github.com:moves-rwth/storm into robustpla

  glatteis

  committed
  34c473f

• iMC changes outside of storm-pars

  glatteis

  committed
  e6e6fdd

• Remove commented out code

  glatteis

  committed
  c1a741a

• Format

  glatteis

  committed
  28ec366

Commits on Nov 11, 2024

• fix verification mode

  glatteis

  committed
  7a7376a

Commits on Nov 12, 2024

• Fix iMDPs

  glatteis

  committed
  217c5a8

• Format

  glatteis

  committed
  b32ec4c

Commits on Nov 18, 2024

• Fix POMDP test segfault

  glatteis

  committed
  2d7239c

• Fix other POMDP test

  glatteis

  committed
  0ee405b

Commits on Nov 19, 2024

• Merge branch 'robustpla-storm' into robustpla

  glatteis

  committed
  3f9e564

• Format and reset testfiles

  glatteis

  committed
  e6f520c

• Default should be to not skip constant deterministic state elimination

  glatteis

  committed
  1184fa5

• Remove z3_api include

  glatteis

  committed
  f4077dc

• Delete disabled tests

  glatteis

  committed
  a8f1952

Commits on Nov 20, 2024

• Remove z3 include

  glatteis

  committed
  c216bfc

• CARL splitting strategy segfaults, so change it?

  glatteis

  committed
  342b237

• Merge branch 'robustpla' of https://github.com/linusheck/storm into robustpla

  glatteis

  committed
  6d2ab9f

• Format

  glatteis

  committed
  164f5c1

Commits on Nov 21, 2024

• Include RationalNumberForward in ParameterRegion.h

  glatteis

  committed
  25d0841

• Format

  glatteis

  committed
  698a5f9

• Maybe RationalNumber(x,y) just doesn't exist for cln

  glatteis

  committed
  59dea93

• Remove RationalNumber mention

  glatteis

  committed
  adb208c

• Fix BinaryDtmcTransformerTest

  glatteis

  committed
  056fbe1

Commits on Nov 26, 2024

• Not sure what the problem is

  glatteis

  committed
  3e09162

Commits on Nov 29, 2024

• Remove print

  glatteis

  committed
  58d4467

• Skip tests if Z3 not available

  glatteis

  committed
  d87be08

• Format >:(

  glatteis

  committed
  05c7b2f

• Fix BinaryDtmcTransformerTest

  glatteis

  committed
  a9397bd

• TEST -> TEST_F

  glatteis

  committed
  3a0e6d0

Commits on Dec 3, 2024

• Warning was inverted >:(

  glatteis

  committed
  8202517