todo_examples/neq_branch.hydlaが正しく動かない

[YunosukeY]

todo_examples/neq_branch.hydlaは，xの初期値が1のときとそうでないときの2つの場合に分かれるはず．

[nikosai]

問題のプログラムは以下。

INIT <=> 0 < x < 2 & [](x'=0).
ANTI <=> [](y = 1).
ASK <=> [](x = 1 => y = 2).

INIT, ANTI << ASK.

[nikosai]

正しくは x の初期値が

• (0,1) or (1, 2)
• 1

の2通りで場合分けになるはずだが、現処理系では

• (-inf,1) or (1, inf)
• 1
• (0,1) or (1,2)
• 1

の4通りが出力されている。

[nikosai]

以下の部分で、x = 1 が成立する場合と不成立の場合とで場合分けが行われている。この際、 phase->additional_constraint_store を経由してMathematicaのグローバル変数 assumptions に x = 1 やその否定が仮定情報として格納される。

HyLaGI/src/simulator/PhaseSimulator.cpp

Lines 887 to 905 in fc5e41d

	if (!unknown_asks.empty()) { /// 最後まで成否が分からないガードがあった場合，
	phase_result_sptr_t branch_state_false = clone_branch_state(phase);
	constraint_t unknown_guard =
	(*unknown_asks.begin())->get_guard(); /// 分からなかったガードを1つ取り
	branch_state_false->additional_constraint_store.add_constraint(constraint_t(
	new Not(unknown_guard))); /// その否定を仮定した分岐を作成．
	phase->parent->todo_list.push_back(branch_state_false);
	phase->additional_constraint_store.add_constraint(
	unknown_guard); /// 今のフェーズにはガードが成り立つという仮定を追加し，
	HYDLA_LOGGER_DEBUG_VAR(branch_state_false->additional_constraint_store);
	backend_->call("addAssumption", true, 1,
	phase->phase_type == INTERVAL_PHASE ? "et" : "en", "",
	&unknown_guard);
	return calculate_closure(phase, trigger_asks, diff_sum, positive_asks,
	negative_asks,
	expanded_always); /// 再び閉包を計算．
	}
	return true;
	}

この assumptions は createVariableMap の引数 assum に渡されるが、その情報はメソッド内で参照されていない。本来、assum の情報も変数への制約として加味するべきである。

HyLaGI/src/backend/mathematica/math_source/math_source.m

Lines 241 to 272 in fc5e41d

	publicMethod[
	createVariableMap,
	cons, vars, assum, pars, current,
	Module[
	{map, tmpCons, succeded = false},
	If[cons === True, Return[{{}}]];
	If[cons === False, Return[{}]];
	tmpCons = removeUnnecessaryConstraints[LogicalExpand[cons], hasVariable];
	If[Head[tmpCons] =!= LogicalOr,
	{tmpCons, succeeded} = tryToTransformConstraints[applyList[LogicalExpand[tmpCons] ], vars]
	];
	simplePrint[tmpCons, succeeded];
	If[!succeeded,
	(* try to solve with parameters *)
	tmpCons = consToDoubleList[cons];
	debugPrint["tmpCons before createMap in createVariableMap", tmpCons];
	tmpCons = Union[Flatten[Map[(createMapForEachCons[#, isVariable, getVariablesWithDerivatives[cons], getParameters[cons]])&, tmpCons], 1]];
	debugPrint["tmpCons after createMap in createVariableMap", tmpCons];
	, tmpCons = applyListToOr[tmpCons];
	tmpCons = Map[(applyList[#])&, tmpCons];
	];
	tmpCons = Map[(adjustExprs[#, isVariable])&, tmpCons];
	debugPrint["tmpCons after adjustExprs in createVariableMap", tmpCons];
	map = Map[(convertExprs[#])&, tmpCons];
	map = Map[(Cases[#, Except[{p[___], _, _}] ])&, map];
	map = ruleOutException[map];
	simplePrint[map];
	map
	]
	];

一方で、 assum を cons に and するなどして上記を修正すると、今度は正しく制約が解けない。

error : math link error: get_integer : 3
(中略)
publicRet$1904: {{{{dx, 1}, 0, "0"}, {{ux, 0}, 2, "0"}, {{ux, 0}, 1, "2"}, {{ux, 0}, Switch[Unequal, Equal, 0, Rule, 0, Less, 1, Greater, 2, LessEqual, 3, GreaterEqual, 4], "1"}}}

不等式をそのまま（パラメタ化せず）Mathematicaに投げるとこうなるらしい。