lp:~opaal-developers/opaal/opaal-ltsmin-succgen
Created by
Mads Chr. Olesen
and last modified
- Get this branch:
- bzr branch lp:~opaal-developers/opaal/opaal-ltsmin-succgen
Members of
opaal developers
can upload to this branch. Log in for directions.
Branch merges
Propose for merging
No branches
dependent on this one.
- opaal developers: Pending requested
-
Diff: 28412 lines (+26932/-139)152 files modifiedREADME (+1/-1)
bin/benchmark.sh (+29/-0)
bin/opaal_draw_statespace (+14/-2)
bin/opaal_ltsmin (+238/-0)
bin/opaal_simulator (+77/-6)
bin/opaal_singlecore (+3/-1)
opaal/clattices/__init__.py (+4/-0)
opaal/clattices/apron.py (+294/-0)
opaal/clattices/base_lattice.py (+57/-0)
opaal/clattices/bitvector.py (+108/-0)
opaal/model_parsers/pyuppaal/__init__.py (+1/-0)
opaal/model_parsers/pyuppaal/analyzer.py (+277/-73)
opaal/model_parsers/pyuppaal/gensuccgen.py (+2017/-0)
opaal/model_parsers/pyuppaal/goal_checker.py (+1/-1)
opaal/model_parsers/pyuppaal/simplify.py (+59/-26)
opaal/model_parsers/pyuppaal/successor_generator.py (+11/-9)
opaal/model_parsers/pyuppaal/util.py (+776/-10)
opaal/passed_waiting_list/lattice_pwlist.py (+4/-1)
opaal/util.py (+25/-0)
tests/SimpleLeader3_mod.xml (+53/-4)
tests/dbmtests/viking1.xml (+37/-0)
tests/explore_all.q (+6/-0)
tests/gensuccgen/cfunc_wrong_ifcond.xml (+33/-0)
tests/gensuccgen/channel_array.xml (+8/-0)
tests/gensuccgen/clock_compare_two.xml (+6/-0)
tests/gensuccgen/clock_equal_guard.xml (+2/-0)
tests/gensuccgen/clock_guard_then_reset.xml (+5/-0)
tests/gensuccgen/clock_guard_then_reset2.xml (+5/-0)
tests/gensuccgen/committed_location.xml (+3/-0)
tests/gensuccgen/committed_urgency.xml (+2/-0)
tests/gensuccgen/committed_urgency2.xml (+2/-0)
tests/gensuccgen/committed_urgency3.xml (+2/-0)
tests/gensuccgen/covered_by.xml (+5/-0)
tests/gensuccgen/duplicate_functions.xml (+24/-0)
tests/gensuccgen/dynamic_sync_sender.xml (+4/-0)
tests/gensuccgen/examples/adding.1.dve (+24/-0)
tests/gensuccgen/examples/adding.1.dve.cpp (+566/-0)
tests/gensuccgen/examples/anderson.1.dve (+36/-0)
tests/gensuccgen/examples/anderson.1.prop2.dve.cpp (+1617/-0)
tests/gensuccgen/examples/chan_op.prom (+31/-0)
tests/gensuccgen/examples/chan_op.prom.spinja.c (+1150/-0)
tests/gensuccgen/examples/run_expression.prom (+20/-0)
tests/gensuccgen/examples/run_expression.prom.spinja.c (+637/-0)
tests/gensuccgen/guard_discrete_clock_mix.xml (+33/-0)
tests/gensuccgen/invariant_delay.xml (+3/-0)
tests/gensuccgen/invariant_disallowed_disjunct.xml (+27/-0)
tests/gensuccgen/invariant_mixed.xml (+27/-0)
tests/gensuccgen/invariant_mixed_disjunct1.xml (+27/-0)
tests/gensuccgen/invariant_mixed_disjunct2.xml (+27/-0)
tests/gensuccgen/invariant_mixed_disjunct3.xml (+28/-0)
tests/gensuccgen/invariant_mixed_disjunct4.xml (+29/-0)
tests/gensuccgen/invariant_var.xml (+20/-0)
tests/gensuccgen/priorities1.xml (+1/-0)
tests/gensuccgen/priorities2.xml (+1/-0)
tests/gensuccgen/priorities3.xml (+3/-0)
tests/gensuccgen/priorities_commited_locs.q (+21/-0)
tests/gensuccgen/priorities_commited_locs.xml (+2/-0)
tests/gensuccgen/signed_var.xml (+25/-0)
tests/gensuccgen/simple1.xml (+7/-0)
tests/gensuccgen/simple_clocktrans1.xml (+7/-0)
tests/gensuccgen/simple_constraints.xml (+5/-0)
tests/gensuccgen/stopwatch1.xml (+1/-0)
tests/gensuccgen/stopwatch2.xml (+1/-0)
tests/gensuccgen/sync_simple_nop.xml (+3/-0)
tests/gensuccgen/unurgent_to_urgent.xml (+6/-0)
tests/gensuccgen/upc_func.xml (+19/-0)
tests/gensuccgen/upc_func_typedef_return.xml (+28/-0)
tests/gensuccgen/upc_functioncall.xml (+10/-0)
tests/gensuccgen/upc_functioncall_parameter.xml (+10/-0)
tests/gensuccgen/upc_functioncall_parameter_typedef.xml (+16/-0)
tests/gensuccgen/upc_guard_func_array.xml (+15/-0)
tests/gensuccgen/upc_guard_true.xml (+7/-0)
tests/gensuccgen/upc_loop_do_while.xml (+31/-0)
tests/gensuccgen/upc_loop_for.xml (+18/-0)
tests/gensuccgen/upc_loop_while.xml (+31/-0)
tests/gensuccgen/upc_metamoc_cache.xml (+132/-0)
tests/gensuccgen/upc_update_array.xml (+7/-0)
tests/gensuccgen/upc_update_func.xml (+20/-0)
tests/gensuccgen/urgent1.xml (+2/-0)
tests/gensuccgen/urgent_bcast_chan1.xml (+4/-0)
tests/gensuccgen/urgent_chan1.xml (+4/-0)
tests/gensuccgen/urgent_chan2.xml (+4/-0)
tests/gensuccgen/urgent_chan_choice.xml (+4/-0)
tests/gensuccgen/urgent_chan_guard.xml (+5/-0)
tests/gensuccgen/urgent_chan_receiver_guard.xml (+5/-0)
tests/gensuccgen/urgent_to_unurgent.xml (+6/-0)
tests/ltl_tests/CSMA_CD/README (+10/-0)
tests/ltl_tests/CSMA_CD/genCSMA_CD.awk (+163/-0)
tests/ltl_tests/csma_input.ltl (+1/-0)
tests/ltl_tests/csma_input_02.xml (+230/-0)
tests/ltl_tests/csma_input_10.xml (+882/-0)
tests/ltl_tests/csma_input_15.xml (+1297/-0)
tests/ltl_tests/csma_input_20.xml (+1712/-0)
tests/ltl_tests/csma_input_25.xml (+2127/-0)
tests/ltl_tests/fischer4.ltl (+1/-0)
tests/ltl_tests/fischer4.xml (+10/-0)
tests/ltl_tests/hddi/README (+10/-0)
tests/ltl_tests/hddi/genHDDI.awk (+165/-0)
tests/ltl_tests/hddi_input_02.ltl (+1/-0)
tests/ltl_tests/hddi_input_02.xml (+203/-0)
tests/ltl_tests/hddi_input_10.ltl (+1/-0)
tests/ltl_tests/hddi_input_10.xml (+923/-0)
tests/ltl_tests/hddi_input_15.xml (+1373/-0)
tests/ltl_tests/hddi_input_20.xml (+1823/-0)
tests/ltl_tests/hypo_subsumption1.xml (+124/-0)
tests/ltl_tests/leader/leader.ltl (+9/-0)
tests/ltl_tests/leader/leader.xml (+92/-0)
tests/ltl_tests/leader/leader2.q (+13/-0)
tests/ltl_tests/leader/leader2.xml (+117/-0)
tests/ltl_tests/leader/leader3.q (+13/-0)
tests/ltl_tests/leader/leader3.xml (+390/-0)
tests/ltl_tests/leader/leader4.q (+13/-0)
tests/ltl_tests/leader/leader4.xml (+109/-0)
tests/ltl_tests/leader/leader5.q (+16/-0)
tests/ltl_tests/leader/leader5.xml (+100/-0)
tests/ltl_tests/li_fischer.xml (+63/-0)
tests/ltl_tests/train-gate.q (+94/-0)
tests/ltl_tests/train-gate.xml (+46/-0)
tests/lubounds_example.xml (+43/-0)
tests/master-election-simple3.xml (+60/-0)
tests/maxconst5.xml (+2/-0)
tests/maxconst_constvar.xml (+28/-0)
tests/maxconst_constvar2.xml (+28/-0)
tests/maxconst_expr1.xml (+28/-0)
tests/maxconst_expr2.xml (+28/-0)
tests/maxconst_expr3.xml (+30/-0)
tests/maxconst_expr4.xml (+28/-0)
tests/maxconst_expr5.xml (+28/-0)
tests/maxconst_expr6.xml (+35/-0)
tests/maxconst_var1.xml (+28/-0)
tests/maxconst_var2.xml (+28/-0)
tests/metamoc/fibcall.xml (+606/-0)
tests/simplify_template_param_const.xml (+27/-0)
tests/simplify_template_param_var.xml (+27/-0)
tests/simplify_template_param_var_typedef.xml (+22/-0)
tests/simplify_template_param_var_typedef2.xml (+26/-0)
tests/sync_twoway_twochoices.xml (+1/-0)
tests/tapaal/train-crossing-bcastdeg2red-5.xml (+1320/-0)
tests/tapaal/train-crossing-optstdred-5.xml (+1465/-0)
tests/tapaal/train-crossing-stdred-5.xml (+17/-0)
tests/test_gensuccgen.py (+1036/-0)
tests/test_gensuccgen_lattice.py (+109/-0)
tests/test_pyuppaal_analyzer.py (+231/-0)
tests/test_pyuppaal_simplify.py (+99/-0)
tests/test_pyuppaal_succgen.py (+172/-2)
tests/train-gate.xml (+165/-0)
tests/vikingtests/viking1.xml (+2/-2)
tests/vikingtests/viking12.xml (+25/-0)
tests/vikingtests/viking15.xml (+31/-0)
tests/vikingtests/viking17.xml (+33/-0)
tests/vikingtests/viking20.xml (+36/-0)
tests/vikingtests/viking4.xml (+1/-1)
Related source package recipes
Branch information
Recent revisions
- 188. By Mads Chr. Olesen
-
fixup gensuccgen StateStruct to correctly allow legacy code to access "locs" vector (which is no longer there)
- 187. By Alfons Laarman <email address hidden>
-
Set FED type to 0 (type 0 has 0 values and hence is a direct type)
- 183. By Mads Chr. Olesen
-
Refactor util.expression
_to_c, and invariant generator; now invariants mixing disjunctions works properly - 180. By Mads Chr. Olesen
-
Add support for invariants with disjunctions that mix discrete and DBM invariants
Branch metadata
- Branch format:
- Branch format 7
- Repository format:
- Bazaar repository format 2a (needs bzr 1.16 or later)
- Stacked on:
- lp:opaal
