diff --git a/tff/domains/decision-system/engines.tff b/tff/domains/decision-system/engines.tff new file mode 100644 index 0000000..41002f2 --- /dev/null +++ b/tff/domains/decision-system/engines.tff @@ -0,0 +1,991 @@ +% Originally contributed by Tyler Olson https://github.com/Rockjack00 + + +% Decision Engines +include('understanding-logic/tff/model/top.tff'). +include('understanding-logic/tff/domains/decision-system/properties.tff'). + +%%%%%% Concepts +%--------------------------------------------------------------------------- +%%% Alternative Array +% A set of alternatives. +%----------------------------------- +tff(alternative_array_decl, type, + alternative_array : concept +). +%----------------------------------- + +%%% Cue Array +% A set of cues to use to make a decision. +%----------------------------------- +tff(cue_array_decl, type, + cue_array : concept +). +%----------------------------------- + +%%% Assessment Matrix +% A matrix of scores of each alternative by each cue. +%----------------------------------- +tff(assessment_matrix_decl, type, + assessment_matrix : concept +). +%----------------------------------- + +%%% Evaluation +% A matix of multi-dimensional values of each alternative. +%----------------------------------- +tff(evaluation_decl, type, + evaluation : concept +). +%----------------------------------- + +%%% WeakOrdering +% A preference relation on a set of alternatives +%----------------------------------- +tff(weak_ordering_decl, type, + weak_ordering : concept +). +%----------------------------------- + +%%% Decision +% A chosen set of alternatives that may or may not have been accepted. +%----------------------------------- +tff(decision_decl, type, + decision: concept +). +%----------------------------------- + + +tff(concepts_are_distinct, axiom, + $distinct(alternative_array, + cue_array, + assessment_matrix, + evaluation, + weak_ordering, + decision) +). + +%--------------------------------------------------------------------------- + + + +%%%%%% Formalisms +%--------------------------------------------------------------------------- +%%% AlternativeArray.msg +% A ROS 2 message decision_msgs/msg/AlternativeArray +%----------------------------------- +tff(alternative_array_msg_decl, type, + alternative_array_msg : formalism +). +%----------------------------------- + +%%% CueArray.msg +% A ROS 2 message decision_msgs/msg/CueArray +%----------------------------------- +tff(cue_array_msg_decl, type, + cue_array_msg : formalism +). +%----------------------------------- + +%%% AssessmentMatrix.msg +% A ROS 2 message decision_msgs/msg/AssessmentMatrix +%----------------------------------- +tff(assessment_matrix_msg_decl, type, + assessment_matrix_msg : formalism +). +%----------------------------------- + +%%% Evaluation.msg +% A ROS 2 message decision_msgs/msg/Evaluation +%----------------------------------- +tff(evaluation_msg_decl, type, + evaluation_msg : formalism +). +%----------------------------------- + +%%% WeakOrdering.msg +% A ROS 2 message decision_msgs/msg/WeakOrdering +%----------------------------------- +tff(weak_ordering_msg_decl, type, + weak_ordering_msg : formalism +). +%----------------------------------- + +%%% Decision.msg +% A ROS 2 message decision_msgs/msg/Decision +%----------------------------------- +tff(decision_msg_decl, type, + decision_msg : formalism +). +%----------------------------------- + +tff(formalisms_are_distinct, axiom, + $distinct(alternative_array_msg, + cue_array_msg, + assessment_matrix_msg, + evaluation_msg, + weak_ordering_msg, + decision_msg) +). + +%--------------------------------------------------------------------------- + + + +%%%%%% Representation Class +%--------------------------------------------------------------------------- +%%% choice set +% A choice set of alternatives, a subset of which may be chosen. +%----------------------------------- +tff(choice_set_decl, type, + choice_set : representation_class +). +%----------------------------------- + +%%% choice +% The chosen set of alternatives. +%----------------------------------- +tff(choice_decl, type, + choice : representation_class +). +%----------------------------------- + +tff(representation_classes_are_distinct, axiom, + $distinct(choice_set, + choice) +). +%--------------------------------------------------------------------------- + + + +%%%%%% Templates +%--------------------------------------------------------------------------- +%%% choice_set +%----------------------------------- +tff(choice_set_template_decl, type, + choice_set_template : template +). + +tff(choice_set_template_no_requirements, axiom, + ~?[R : requirement]: + is_part_of(R, choice_set_template) +). + +tff(choice_set_template_no_creator_requirements, axiom, + ~?[E: engine]: + template_has_creator_requirement(choice_set_template, E) +). + +% TODO: combine this with take_template_concept? +% Right now double implication is too strong +tff(choice_set_template_concept, axiom, +( + % It only has this requirement + template_has_concept_requirement(choice_set_template, alternative_array) + & + % It has no other concept requirements + ![C : concept]: + ( + template_has_concept_requirement(choice_set_template, C) + => + C = alternative_array + ) +) +). + +tff(choice_set_template_formalism, axiom, + template_formalism_requirement(choice_set_template) = alternative_array_msg +). + +% Using this particular set of alternatives as a choice set +% +% TODO: Need an engine that adds a representation class to sets of alternatives (this will be GetAlternatives :D) +% +tff(choice_set_template_representation_class, axiom, + ![R : representation_class]: + ( + template_has_representation_class_requirement(choice_set_template, R) + <=> + R = choice_set + ) +). + +tff(choice_set_template_no_location_requirements, axiom, + ~?[SPT: spacetime_point]: + template_has_location_requirement(choice_set_template, SPT) +). + +tff(choice_set_template_no_extent_requirements, axiom, + ~?[E: extent]: + template_has_extent_requirement(choice_set_template, E) +). +%----------------------------------- + +%%% cue_array +%----------------------------------- +tff(cue_array_template_decl, type, + cue_array_template : template +). + +tff(cue_array_template_no_requirements, axiom, + ~?[R : requirement]: + is_part_of(R, cue_array_template) +). + +tff(cue_array_template_no_creator_requirements, axiom, + ~?[E: engine]: + template_has_creator_requirement(cue_array_template, E) +). + +tff(cue_array_template_concept, axiom, + ![C : concept]: + ( + template_has_concept_requirement(cue_array_template, C) + <=> + C = cue_array + ) +). + +tff(cue_array_template_formalism, axiom, + template_formalism_requirement(cue_array_template) = cue_array_msg +). + +tff(cue_array_template_representation_class, axiom, + ~?[R : representation_class]: + template_has_representation_class_requirement(cue_array_template, R) +). + +tff(cue_array_template_no_location_requirements, axiom, + ~?[SPT: spacetime_point]: + template_has_location_requirement(cue_array_template, SPT) +). + +tff(cue_array_template_no_extent_requirements, axiom, + ~?[E: extent]: + template_has_extent_requirement(cue_array_template, E) +). +%----------------------------------- + +%%% assessment_matrix +%----------------------------------- +tff(assessment_matrix_template_decl, type, + assessment_matrix_template : template +). + +tff(assessment_matrix_template_no_requirements, axiom, + ~?[R : requirement]: + is_part_of(R, assessment_matrix_template) +). + +tff(assessment_matrix_template_no_creator_requirements, axiom, + ~?[E: engine]: + template_has_creator_requirement(assessment_matrix_template, E) +). + +tff(assessment_matrix_template_concept, axiom, + ![C : concept]: + ( + template_has_concept_requirement(assessment_matrix_template, C) + <=> + C = assessment_matrix + ) +). + +tff(assessment_matrix_template_formalism, axiom, + template_formalism_requirement(assessment_matrix_template) = assessment_matrix_msg +). + +tff(assessment_matrix_template_representation_class, axiom, + ~?[R : representation_class]: + template_has_representation_class_requirement(assessment_matrix_template, R) +). + +tff(assessment_matrix_template_no_location_requirements, axiom, + ~?[SPT: spacetime_point]: + template_has_location_requirement(assessment_matrix_template, SPT) +). + +tff(assessment_matrix_template_no_extent_requirements, axiom, + ~?[E: extent]: + template_has_extent_requirement(assessment_matrix_template, E) +). +%----------------------------------- + +%%% evaluation +%----------------------------------- +tff(evaluation_template_decl, type, + evaluation_template : template +). + +tff(evaluation_template_no_requirements, axiom, + ~?[R : requirement]: + is_part_of(R, evaluation_template) +). + +tff(evaluation_template_no_creator_requirements, axiom, + ~?[E: engine]: + template_has_creator_requirement(evaluation_template, E) +). + +tff(evaluation_template_concept, axiom, + ![C : concept]: + ( + template_has_concept_requirement(evaluation_template, C) + <=> + C = evaluation + ) +). + +tff(evaluation_template_formalism, axiom, + template_formalism_requirement(evaluation_template) = evaluation_msg +). + +tff(evaluation_template_representation_class, axiom, + ~?[R : representation_class]: + template_has_representation_class_requirement(evaluation_template, R) +). + +tff(evaluation_template_no_location_requirements, axiom, + ~?[SPT: spacetime_point]: + template_has_location_requirement(evaluation_template, SPT) +). + +tff(evaluation_template_no_extent_requirements, axiom, + ~?[E: extent]: + template_has_extent_requirement(evaluation_template, E) +). +%----------------------------------- + +%%% weak_ordering +%----------------------------------- +tff(weak_ordering_template_decl, type, + weak_ordering_template : template +). + +tff(weak_ordering_template_no_requirements, axiom, + ~?[R : requirement]: + is_part_of(R, weak_ordering_template) +). + +tff(weak_ordering_template_no_creator_requirements, axiom, + ~?[E: engine]: + template_has_creator_requirement(weak_ordering_template, E) +). + +tff(weak_ordering_template_concept, axiom, + ![C : concept]: + ( + template_has_concept_requirement(weak_ordering_template, C) + <=> + C = weak_ordering + ) +). + +tff(weak_ordering_template_formalism, axiom, + template_formalism_requirement(weak_ordering_template) = weak_ordering_msg +). + +tff(weak_ordering_template_representation_class, axiom, + ~?[R : representation_class]: + template_has_representation_class_requirement(weak_ordering_template, R) +). + +tff(weak_ordering_template_no_location_requirements, axiom, + ~?[SPT: spacetime_point]: + template_has_location_requirement(weak_ordering_template, SPT) +). + +tff(weak_ordering_template_no_extent_requirements, axiom, + ~?[E: extent]: + template_has_extent_requirement(weak_ordering_template, E) +). +%----------------------------------- + +%%% choice +%----------------------------------- +tff(choice_template_decl, type, + choice_template : template +). + +tff(choice_template_no_requirements, axiom, + ~?[R : requirement]: + is_part_of(R, choice_template) +). + +tff(choice_template_no_creator_requirements, axiom, + ~?[E: engine]: + template_has_creator_requirement(choice_template, E) +). + +tff(choice_template_concept, axiom, + ![C : concept]: + ( + template_has_concept_requirement(choice_template, C) + <=> + C = alternative_array + ) +). + +tff(choice_template_formalism, axiom, + template_formalism_requirement(choice_template) = alternative_array_msg +). + +tff(choice_template_representation_class, axiom, + ![R : representation_class]: + ( + template_has_representation_class_requirement(choice_template, R) + <=> + R = choice + ) +). + +tff(choice_template_no_location_requirements, axiom, + ~?[SPT: spacetime_point]: + template_has_location_requirement(choice_template, SPT) +). + +tff(choice_template_no_extent_requirements, axiom, + ~?[E: extent]: + template_has_extent_requirement(choice_template, E) +). +%----------------------------------- + +tff(templates_are_distinct, axiom, + $distinct(choice_set_template, + cue_array_template, + assessment_matrix_template, + evaluation_template, + weak_ordering_template, + choice_template) +). + +%--------------------------------------------------------------------------- + + + +%%%%%% Engines +%--------------------------------------------------------------------------- +%%% UpdateAlternatives +% elim - assume all, eliminate until desired (diminishing) +% keep_policy = taken, capacity = 0 +% (used for eliminate-by-aspects) +%----------------------------------- +tff(update_alternatives_elim_engine_decl, type, + update_alternatives_elim_engine : engine +). + +tff(update_alternatives_elim_engine_output_formalism, axiom, + output_modelet_formalism(update_alternatives_elim_engine) = alternative_array_msg +). + +tff(update_alternatives_elim_engine_output_concept, axiom, + ![C : concept]: + ( + is_output_modelet_concept(update_alternatives_elim_engine, C) + <=> + C = alternative_array + ) +). + +tff(update_alternatives_elim_engine_output_representation_class, axiom, + ![R : representation_class]: + ( + is_output_modelet_representation_class(update_alternatives_elim_engine, R) + <=> + R = choice_set + ) +). + +%TODO: update_alternatives_elim_engine has no inputs, find a formulation. + +%----------------------------------- + +%%% UpdateCues +% iter_one - Use and lose one cue per round (dynamic) +% reuse = False, iter_add = 1 +% (used for eliminate-by-aspects) +%----------------------------------- +% tff(update_cues_iter_one_engine_decl, type, +% update_cues_iter_one_engine : engine +% ). + +tff(update_cues_take_the_best_engine_decl, type, + update_cues_take_the_best_engine : engine +). + +tff(update_cues_engine_output_formalisms, axiom, +% output_modelet_formalism(update_cues_iter_one_engine) = cue_array_msg +% & + output_modelet_formalism(update_cues_take_the_best_engine) = cue_array_msg +). + +tff(update_cues_iter_one_engine_output_concept, axiom, + ![C : concept]: + ( + ( +% is_output_modelet_concept(update_cues_iter_one_engine, C) +% | + is_output_modelet_concept(update_cues_take_the_best_engine, C) + ) + <=> + C = cue_array + ) +). + +tff(update_cues_iter_one_engine_output_representation_class, axiom, + ~?[R : representation_class]: + ( +% is_output_modelet_representation_class(update_cues_iter_one_engine, R) +% | + is_output_modelet_representation_class(update_cues_take_the_best_engine, R) + ) +). + +%TODO: update_cues_take_the_best_engine has no inputs, find a formulation. + +%----------------------------------- + +%%% Assess +%----------------------------------- +tff(assess_engine_decl, type, + assess_engine : engine +). + +tff(assess_engine_output_formalism, axiom, + output_modelet_formalism(assess_engine) = assessment_matrix_msg +). + +tff(assess_engine_output_concept, axiom, + ![C : concept]: + ( + is_output_modelet_concept(assess_engine, C) + <=> + C = assessment_matrix + ) +). + +% TODO: Right now the AssessmentMatrix is modeled as an atomic modelet, but it could +% be modeled with a representation class... +tff(assess_engine_output_representation_class, axiom, + ~?[R : representation_class]: + is_output_modelet_representation_class(assess_engine, R) +). + +tff(assess_engine_defined_input, axiom, + defines_input2(choice_set_template, cue_array_template, assess_engine) +). + + +%----------------------------------- + +%%% Aggregate +%----------------------------------- +tff(aggregate_preferences_engine_decl, type, + aggregate_preferences_engine : engine +). + +tff(aggregate_utility_boolean_engine_decl, type, + aggregate_utility_boolean_engine : engine +). + +tff(aggregate_utility_signed_engine_decl, type, + aggregate_utility_signed_engine : engine +). + +tff(aggregate_utility_sum_engine_decl, type, + aggregate_utility_sum_engine : engine +). + +% TODO: implement multi-value utility +% tff(aggregate_multi_value_utility_engine_decl, type, +% aggregate_multi_value_utility_engine : engine +% ). + +tff(aggregate_engines_output_formalism, axiom, + output_modelet_formalism(aggregate_preferences_engine) = evaluation_msg + & + output_modelet_formalism(aggregate_utility_boolean_engine) = evaluation_msg + & + output_modelet_formalism(aggregate_utility_signed_engine) = evaluation_msg + & + output_modelet_formalism(aggregate_utility_sum_engine) = evaluation_msg + % & + % output_modelet_formalism(aggregate_multi_value_utility_engine) = evaluation_msg +). + +tff(aggregate_engines_output_concept, axiom, + ![C : concept]: + ( + ( + is_output_modelet_concept(aggregate_preferences_engine, C) + | + is_output_modelet_concept(aggregate_utility_boolean_engine, C) + | + is_output_modelet_concept(aggregate_utility_signed_engine, C) + | + is_output_modelet_concept(aggregate_utility_sum_engine, C) + % | + % is_output_modelet_concept(aggregate_multi_value_utility_engine, C) + ) + <=> + C = evaluation + ) +). + +tff(aggregate_engines_output_representation_class, axiom, + ~?[R : representation_class]: + ( + is_output_modelet_representation_class(aggregate_preferences_engine, R) + | + is_output_modelet_representation_class(aggregate_utility_boolean_engine, R) + | + is_output_modelet_representation_class(aggregate_utility_signed_engine, R) + | + is_output_modelet_representation_class(aggregate_utility_sum_engine, R) + % | + % is_output_modelet_representation_class(aggregate_multi_value_utility_engine, R) + ) +). + + + +tff(aggregate_preferences_engine_defined_input, axiom, + defines_input1(assessment_matrix_template, aggregate_preferences_engine) +). + +tff(aggregate_utility_boolean_engine_defined_input, axiom, + defines_input1(assessment_matrix_template, aggregate_utility_boolean_engine) +). + +tff(aggregate_utility_signed_engine_defined_input, axiom, + defines_input1(assessment_matrix_template, aggregate_utility_signed_engine) +). + + +tff(aggregate_utility_sum_engine_defined_input, axiom, + defines_input1(assessment_matrix_template, aggregate_utility_sum_engine) +). + + +%tff(aggregate_multi_value_utility_engine_defined_input, axiom, +% defines_input1(assessment_matrix_template, aggregate_multi_value_utility_engine) +%). + +%----------------------------------- + +%%% Order +%----------------------------------- +tff(order_condorcet_engine_decl, type, + order_condorcet_engine : engine +). + +tff(order_dominating_engine_decl, type, + order_dominating_engine : engine +). + +tff(order_lexicographical_engine_decl, type, + order_lexicographical_engine : engine +). + +tff(order_engines_output_formalism, axiom, + output_modelet_formalism(order_condorcet_engine) = weak_ordering_msg + & + output_modelet_formalism(order_dominating_engine) = weak_ordering_msg + & + output_modelet_formalism(order_lexicographical_engine) = weak_ordering_msg +). + +tff(order_engines_output_concept, axiom, + ![C : concept]: + ( + ( + is_output_modelet_concept(order_condorcet_engine, C) + | + is_output_modelet_concept(order_dominating_engine, C) + | + is_output_modelet_concept(order_lexicographical_engine, C) + ) + <=> + C = weak_ordering + ) +). + +tff(order_engines_output_representation_class, axiom, + ~?[R : representation_class]: + ( + is_output_modelet_representation_class(order_condorcet_engine, R) + | + is_output_modelet_representation_class(order_dominating_engine, R) + | + is_output_modelet_representation_class(order_lexicographical_engine, R) + ) +). + + +tff(order_condorcet_engine_defined_input, axiom, + defines_input1(evaluation_template, order_condorcet_engine) +). + +tff(order_dominating_engine_defined_input, axiom, + defines_input1(evaluation_template, order_dominating_engine) +). + +tff(order_lexicographical_engine_defined_input, axiom, + defines_input1(evaluation_template, order_lexicographical_engine) +). + +%----------------------------------- + +%%% Take +%----------------------------------- +tff(take_best_engine_decl, type, + take_best_engine : engine +). + +tff(eliminate_worst_engine_decl, type, + eliminate_worst_engine : engine +). + +tff(take_engines_output_formalism, axiom, + output_modelet_formalism(take_best_engine) = alternative_array_msg + & + output_modelet_formalism(eliminate_worst_engine) = alternative_array_msg +). + + +% TODO: combine this with get/update_alternatives_output_concept? +% Right now double implication is too strong +tff(take_engines_output_concept, axiom, + ( + is_output_modelet_concept(take_best_engine, alternative_array) + & + is_output_modelet_concept(eliminate_worst_engine, alternative_array) + & + ![C : concept]: + ( + ( + is_output_modelet_concept(take_best_engine, C) + | + is_output_modelet_concept(eliminate_worst_engine, C) + ) + => + C = alternative_array + ) + ) +). + +tff(take_engines_output_representation_class, axiom, + ( + % Right now these statements are redudant with the universal quantifier, + % but help make it faster. + is_output_modelet_representation_class(take_best_engine, choice) + & + is_output_modelet_representation_class(eliminate_worst_engine, choice) + & + ![R : representation_class]: + ( + ( + is_output_modelet_representation_class(take_best_engine, R) + | + is_output_modelet_representation_class(eliminate_worst_engine, R) + ) + <=> + R = choice + ) + ) +). + +% TODO: It is not generally true that take_best imparts absolute size, but it is +% true with the default configuration. This is currently the only possible configuration +% by the heuristic assembly node so for now it works. +tff(take_best_imparts_absolute_size_prop, axiom, + ( + % This is redundant, but helps with performance + engine_imparts_output_property(take_best_engine, absolute_size_prop) + & + ! [P: property]: + ( + engine_imparts_output_property(take_best_engine, P) + <=> + P = absolute_size_prop + ) + ) +). + + +tff(take_best_engine_defined_input, axiom, + defines_input1(weak_ordering_template, take_best_engine) +). + +tff(eliminate_worst_engine_defined_input, axiom, + defines_input1(weak_ordering_template, eliminate_worst_engine) +). + +%----------------------------------- + +%%% Accept +%----------------------------------- +tff(accept_always_engine_decl, type, + accept_always_engine : engine +). + +tff(accept_dominating_engine_decl, type, + accept_dominating_engine : engine +). + +tff(accept_satisficing_engine_decl, type, + accept_satisficing_engine : engine +). + +tff(accept_size_engine_decl, type, + accept_size_engine : engine +). + + + +tff(accept_size_engine_has_properties, axiom, + ( + engine_has_property(accept_size_engine, n_parameter_prop) + & + engine_has_property(accept_size_engine, relation_parameter_prop) + %%% RESUME + + % & + % + % % This can enforce a size desired by the gap by setting the parameters. + % ![N: $real]: + % ( + % ( + % has_value(n_parameter_prop) = N + % & + % has_value(relation_parameter_prop) = 1.0 % Assume 1 means '=' for now (like an enum) + % ) + % <=> + % ( + % % Allow a model of known properties to enforce the property from this engine. + % ?[M: modelet]: + % ( + % modelet_has_creator(M, accept_size_engine) + % & + % modelet_has_property(M, absolute_size_prop) + % & + % has_value(absolute_size_prop) = N + % ) + % => + % engine_imparts_output_property(accept_size_engine, absolute_size_prop) + % ) + % ) + ) +). + + +tff(accept_size_imparts_absolute_size_prop, axiom, + ( + % This is redundant, but helps with performance + engine_imparts_output_property(accept_size_engine, absolute_size_prop) + & + ! [P: property]: + ( + engine_imparts_output_property(accept_size_engine, P) + <=> + P = absolute_size_prop + ) + ) +). + + +% TODO: consider outputting a boolean instead of a whole decision message +% That is more in the spirit of what is going on, and lets the 'decision +% engine' (behavior tree) output decisions. +% That being said, would we rather the 'decision engine' output a useful +% modelet (unpacked) instead? +tff(accept_engines_output_formalism, axiom, + output_modelet_formalism(accept_always_engine) = decision_msg + & + output_modelet_formalism(accept_dominating_engine) = decision_msg + & + output_modelet_formalism(accept_satisficing_engine) = decision_msg + & + output_modelet_formalism(accept_size_engine) = decision_msg +). + +% TODO: see above +tff(accept_engines_output_concept, axiom, + ( + % Right now these statements are redudant with the universal quantifier, + % but help make it faster. + is_output_modelet_concept(accept_always_engine, decision) + & + is_output_modelet_concept(accept_dominating_engine, decision) + & + is_output_modelet_concept(accept_satisficing_engine, decision) + & + is_output_modelet_concept(accept_size_engine, decision) + & + ![C : concept]: + ( + ( + is_output_modelet_concept(accept_always_engine, C) + | + is_output_modelet_concept(accept_dominating_engine, C) + | + is_output_modelet_concept(accept_satisficing_engine, C) + | + is_output_modelet_concept(accept_size_engine, C) + ) + <=> + C = decision + ) + ) +). + +% TODO: see above, it would mean that the boolean takes the representation of +% accepting or rejecting a decision... +tff(accept_engines_output_representation_class, axiom, + ~?[R : representation_class]: + ( + is_output_modelet_representation_class(accept_always_engine, R) + | + is_output_modelet_representation_class(accept_dominating_engine, R) + | + is_output_modelet_representation_class(accept_satisficing_engine, R) + | + is_output_modelet_representation_class(accept_size_engine, R) + ) +). + + +tff(accept_always_engine_defined_input, axiom, + defines_input1(choice_template, accept_always_engine) +). + +tff(accept_dominating_engine_defined_input, axiom, + defines_input1(choice_template, accept_dominating_engine) +). + +tff(accept_satisficing_engine_defined_input, axiom, + defines_input1(choice_template, accept_satisficing_engine) +). + +tff(accept_size_engine_defined_input, axiom, + defines_input1(choice_template, accept_size_engine) +). + + +%----------------------------------- + +% These decision engines transit the "absolute_size" property. +% i.e. If some other engine ensures the absolute size of a chosen set, then this +% engine will ensure that is also a property of the decision. +tff(properties_are_transited_through_engines, axiom, + engine_transits_property(accept_always_engine, absolute_size_prop) + & + engine_transits_property(accept_dominating_engine, absolute_size_prop) + & + engine_transits_property(accept_satisficing_engine, absolute_size_prop) + & + engine_transits_property(accept_size_engine, absolute_size_prop) +). + + +%--------------------------------------------------------------------------- diff --git a/tff/domains/decision-system/properties.tff b/tff/domains/decision-system/properties.tff new file mode 100644 index 0000000..cede83a --- /dev/null +++ b/tff/domains/decision-system/properties.tff @@ -0,0 +1,53 @@ +% Originally contributed by Tyler Olson https://github.com/Rockjack00 + +% Decision properties for fixed parameters +%include('/understanding-logic/tff/model/properties.tff'). + +%%%%%% Datatypes +%--------------------------------------------------------------------------- +%%% Choice Size +% TODO: This is not a datatype, it is a phenomenon. but right now there's not a way to express that... +%----------------------------------- +tff(choice_size_datatype_decl, type, + choice_size_datatype : proptype +). +%----------------------------------- + +%--------------------------------------------------------------------------- + + + +%%%%%% Properties +%--------------------------------------------------------------------------- +%%% Decision Properties +%----------------------------------- +tff(absolute_size_prop_decl, type, + absolute_size_prop : property +). + +tff(absolute_size_prop_datatype, axiom, + type_of_property(absolute_size_prop) = choice_size_datatype +). + +%%% Choice properties +%----------------------------------- +tff(absolute_size_prop_decl, type, + absolute_size_prop : property +). + +tff(n_parameter_prop_decl, type, + n_parameter_prop : property +). + +tff(relation_parameter_prop_decl, type, + relation_parameter_prop : property +). + +%----------------------------------- + +tff(properties_are_distinct, axiom, + $distinct(absolute_size_prop, + n_parameter_prop, + relation_parameter_prop + ) +). diff --git a/tff/model/engines.tff b/tff/model/engines.tff index 7344b6d..341df8f 100644 --- a/tff/model/engines.tff +++ b/tff/model/engines.tff @@ -26,6 +26,11 @@ tff(decl_engine_output_properties, type, tff(decl_engine_imparts_output_properties, type, engine_imparts_output_property: (engine * property) > $o ). + +% Engine outputs may retain properties +tff(engine_transits_property_decl, type, + engine_transits_property : (engine * property) > $o +). %--- tff(decl_engine_output_formalism, type, @@ -79,13 +84,13 @@ tff(formally_equivalent, axiom, modelet_models_concept(M, C) ) & -% ![R: representation_class]: -% ( % Equivalence of processing model classes -% template_has_representation_class_requirement(T, R) -% => -% modelet_has_representation_class(M, R) -% ) -% & + ![R: representation_class]: + ( % Equivalence of processing model classes + template_has_representation_class_requirement(T, R) + => + modelet_has_representation_class(M, R) + ) + & ! [SPT : spacetime_point]: ( template_has_location_requirement(T, SPT) @@ -137,3 +142,21 @@ tff(axiom_modelet_matches_template, axiom, inputs_match(M, T) ) ). + +% Engines can conform to requirements +tff(decl_engine_meets_requirement, type, + engine_meets_requirement: (engine * requirement) > $o +). + +tff(axiom_engine_meets_requirement, axiom, + ! [E : engine, R : requirement, P: property]: + ( + ( + engine_has_property(E, P) % match engine to property + & + property_meets_requirement(P, R) + ) + => + engine_meets_requirement(E, R) + ) +). diff --git a/tff/model/one.tff b/tff/model/one.tff index d213e8a..683bb68 100644 --- a/tff/model/one.tff +++ b/tff/model/one.tff @@ -20,12 +20,14 @@ tff(decl_exertable1, type, ). % Modelets are exertable by Engines (no sets) 1 tff(axiom_modelet_is_exertable1, axiom, - ![M: modelet, T: template, E: engine]: + ![M: modelet, T: template, E: engine, R: requirement]: ( ( inputs_match(M, T) & defines_input1(T, E) + & + (is_active(R) => engine_meets_requirement(E, R)) ) => exertable1(E, M) @@ -132,3 +134,21 @@ tff(axiom_engine_may_impart_property1, axiom, ). + +tff(axiom_engine_may_transit_property1, axiom, + ! [E: engine, IM1: modelet, OM: modelet, P: property]: + ( + ( + exertable1(E, IM1) + & + exert1(E, IM1) = OM + & + engine_transits_property(E, P) + & + modelet_has_property(IM1, P) + ) + => + modelet_has_property(OM, P) + ) +). + diff --git a/tff/model/properties-and-requirements.tff b/tff/model/properties-and-requirements.tff index 44b43fe..64e7938 100644 --- a/tff/model/properties-and-requirements.tff +++ b/tff/model/properties-and-requirements.tff @@ -25,6 +25,9 @@ tff(decl_type_of_r, type, tff(decl_requirement_range, type, is_permissible: (requirement * $real) > $o). +% Requirements can be active, when applied to engines +tff(decl_requirement_active, type, + is_active: (requirement) > $o). tff(property_meets_requirement_decl, type, property_meets_requirement : (property * requirement) > $o diff --git a/tff/model/sets.tff b/tff/model/sets.tff index d1faf6c..c2a6cbf 100644 --- a/tff/model/sets.tff +++ b/tff/model/sets.tff @@ -222,6 +222,30 @@ tff(axiom_engine_may_impart_property, axiom, ) ). +%%%%%% Transitive properties +%--------------------------------------------------------------------------- +% An engine transits a property from any of its inputs to its output. +% That is if any of its inputs have some property P, then its output will also +% have that property P. +tff(axiom_engine_transits_property, axiom, + ![E : engine, P : property, MS : modelet_set]: + ( + ( + exertable(E, MS) + & + engine_transits_property(E, P) + & + ?[Mparent : modelet]: + ( + is_in_modelet_set(Mparent, MS) + & + modelet_has_property(Mparent, P) + ) + ) + => + modelet_has_property(exert(E, MS), P) + ) +). %Engines produce reliable output %tff(axiom_engine_reliability, axiom, diff --git a/tff/model/three.tff b/tff/model/three.tff index 0cb6928..4ae80fb 100644 --- a/tff/model/three.tff +++ b/tff/model/three.tff @@ -19,7 +19,7 @@ tff(decl_exertable3, type, ). % Modelets are exertable by Engines (no sets) 3 tff(axiom_modelet_is_exertable3, axiom, - ![M1: modelet, M2: modelet, M3: modelet, T1: template, T2: template, T3: template, E: engine]: + ![M1: modelet, M2: modelet, M3: modelet, T1: template, T2: template, T3: template, E: engine, R: requirement]: ( ( inputs_match(M1, T1) @@ -29,6 +29,8 @@ tff(axiom_modelet_is_exertable3, axiom, inputs_match(M3, T3) & defines_input3(T1, T2, T3, E) + & + (is_active(R) => engine_meets_requirement(E, R)) ) => exertable3(E, M1, M2, M3) @@ -133,3 +135,28 @@ tff(axiom_engine_may_impart_property3, axiom, modelet_has_property(OM, P) ) ). + + + +tff(axiom_engine_may_transit_property3, axiom, + ! [E: engine, IM1: modelet, IM2: modelet, IM3: modelet, OM: modelet, P: property]: + ( + ( + exertable3(E, IM1, IM2, IM3) + & + exert3(E, IM1, IM2, IM3) = OM + & + engine_transits_property(E, P) + & + ( + modelet_has_property(IM1, P) + | + modelet_has_property(IM2, P) + | + modelet_has_property(IM3, P) + ) + ) + => + modelet_has_property(OM, P) + ) +). diff --git a/tff/model/two.tff b/tff/model/two.tff index 4bd834a..64069ec 100644 --- a/tff/model/two.tff +++ b/tff/model/two.tff @@ -20,7 +20,7 @@ tff(decl_exertable2, type, ). % Modelets are exertable by Engines (no sets) 2 tff(axiom_modelet_is_exertable2, axiom, - ![M1: modelet, M2: modelet, T1: template, T2: template, E: engine]: + ![M1: modelet, M2: modelet, T1: template, T2: template, E: engine, R: requirement]: ( ( inputs_match(M1, T1) @@ -28,6 +28,8 @@ tff(axiom_modelet_is_exertable2, axiom, inputs_match(M2, T2) & defines_input2(T1, T2, E) + & + (is_active(R) => engine_meets_requirement(E, R)) ) => exertable2(E, M1, M2) @@ -131,3 +133,24 @@ tff(axiom_engine_may_impart_property2, axiom, modelet_has_property(OM, P) ) ). + +tff(axiom_engine_may_transit_property2, axiom, + ! [E: engine, IM1: modelet, IM2: modelet, OM: modelet, P: property]: + ( + ( + exertable2(E, IM1, IM2) + & + exert2(E, IM1, IM2) = OM + & + engine_transits_property(E, P) + & + ( + modelet_has_property(IM1, P) + | + modelet_has_property(IM2, P) + ) + ) + => + modelet_has_property(OM, P) + ) +). diff --git a/tff/tests/test-decision-engines.tff b/tff/tests/test-decision-engines.tff new file mode 100644 index 0000000..ce8a7b0 --- /dev/null +++ b/tff/tests/test-decision-engines.tff @@ -0,0 +1,112 @@ +% Test Decision engines +include('understanding-logic/tff/domains/decision-system/engines.tff'). + + +%%%%%% Input Modelets +%--------------------------------------------------------------------------- + +%%% Alternatives (assume given for now) +% A set of alternatives to choose from - the choice set. +%----------------------------------- +tff(given_alternatives_decl, type, + given_alternatives_modelet : modelet +). + +tff(given_alternatives_modelet_creator, axiom, + ~?[E : engine]: + modelet_has_creator(given_alternatives_modelet, E) +). + +%tff(given_alternatives_modelet_parents, axiom, +% parents_of_modelet(given_alternatives_modelet) = empty_ms +%). + +% TODO: This cannot be a biconditional because other modelets (namely the choice/chosen set) +% could also model the `alternative_array` concept +tff(given_alternatives_modelet_models_alternative_array, axiom, + ( + modelet_models_concept(given_alternatives_modelet, alternative_array) + & + ![C : concept]: + ( + modelet_models_concept(given_alternatives_modelet, C) + => + C = alternative_array + ) + ) +). + +tff(given_alternatives_modelet_formalism, axiom, + formalism_of_modelet(given_alternatives_modelet) = alternative_array_msg +). + +% TODO: This should probably not be a biconditional in general, but is fine for now. +tff(given_alternatives_modelet_representation_class, axiom, + ![R : representation_class]: + ( + modelet_has_representation_class(given_alternatives_modelet, R) + <=> + R = choice_set + ) +). + +%----------------------------------- + +%%% Cues (assume given for now) +% A set of cues to use to assess the alternatives. +%----------------------------------- +tff(given_cues_modelet_decl, type, + given_cues_modelet : modelet +). + +tff(given_cues_modelet_creator, axiom, + ~?[E : engine]: + modelet_has_creator(given_cues_modelet, E) +). + +%tff(given_cues_modelet_parents, axiom, +% parents_of_modelet(given_cues_modelet) = empty_ms +%). + +% TODO: This should probably not be a biconditional in general, but is fine for now. +tff(given_cues_modelet_models_cue_array, axiom, + ![C : concept]: + ( + modelet_models_concept(given_cues_modelet, C) + <=> + C = cue_array + ) +). + +tff(given_cues_modelet_formalism, axiom, + formalism_of_modelet(given_cues_modelet) = cue_array_msg +). +%----------------------------------- + + +% Initial understanding +%tff(initial_understanding_decl, type, +% ius : modelet_set +%). + +%tff(initial_understanding_set_membership, axiom, +% ( +% ![M : modelet]: +% ( +% is_in_modelet_set(M, ius) +% <=> +% ( +% M = given_alternatives_modelet +% | +% M = given_cues_modelet +% ) +% ) +% ) +%). + +tff(input_modelets_are_distinct, axiom, + $distinct(given_alternatives_modelet, + given_cues_modelet) +). + +%--------------------------------------------------------------------------- diff --git a/tff/tests/test-decision-questions.tff b/tff/tests/test-decision-questions.tff new file mode 100644 index 0000000..318b952 --- /dev/null +++ b/tff/tests/test-decision-questions.tff @@ -0,0 +1,136 @@ +% Originally contributed by Tyler Olson https://github.com/Rockjack00 + +% Test Decision engine questions +include('understanding-logic/tff/domains/decision-system/engines.tff'). +include('understanding-logic/tff/tests/test-decision-engines.tff'). +tff(no_engine_requirements, axiom, + ![R: requirement]: + ~is_active(R) +). + + +%%% Do the input modelets exist? +%% Output: +% SZS answers Tuple [[M1->given_alternatives_modelet,M2->given_cues_modelet]|_] for test-decision-questions +% +% tff(question_decl, question, +% ?[M1 : modelet, M2: modelet]: +% ( +% modelet_models_concept(M1, alternative_array) +% & +% modelet_models_concept(M2, cue_array) +% ) +% ). + + +%%% Test assess +%%% Output +% SZS answers Tuple [([M->exert(assess_engine,ius)]|[M->exert(assess_engine,ius)])|_] for test-decision-questions +% +% tff(question_decl, question, +% ?[M : modelet]: +% ( +% modelet_models_concept(M, assessment_matrix) +% ) +% ). + + +%%% Test aggregate +%%% Output +% SZS answers Tuple [(∀X0.[M->exert(aggregate_preferences_engine,s(exert(assess_engine,ius),X0))]|∀X0.[M->exert(aggregate_utility_boolean_engine,s(exert(assess_engine,ius),X0))]|∀X0.[M->exert(aggregate_utility_sum_engine,s(exert(assess_engine,ius),X0))]|∀X0.[M->exert(aggregate_utility_signed_engine,s(exert(assess_engine,ius),X0))])|_] for test-decision-questions +% +% tff(question_decl, question, +% ?[M : modelet]: +% ( +% modelet_models_concept(M, evaluation) +% ) +% ). + + +%%% Test order +% +% Solved with this strategy: +% dis+1010_1:4_drc=ordering:aac=none:abs=on:atotf=0.5:avsq=on:avsqc=2:avsqr=215,247:bsd=on:erd=off:fde=none:gve=cautious:newcnf=on:nwc=5.0:rnwc=on:sac=on:sas=z3:sp=const_min:tgt=ground:thsq=on:thsqc=64:thsqr=1,4:i=59848:si=on:rawr=on:rtra=on_0 +% +% simplified to -s 1010 +% +%%% Output +% SZS answers Tuple [(∀X1,X0.[M->exert(order_condorcet_engine,s(exert(aggregate_preferences_engine,s(exert(assess_engine,ius),X0)),X1))]|∀X1,X0.[M->exert(order_lexicographical_engine,s(exert(aggregate_preferences_engine,s(exert(assess_engine,ius),X0)),X1))]|∀X1,X0.[M->exert(order_dominating_engine,s(exert(aggregate_preferences_engine,s(exert(assess_engine,ius),X0)),X1))]|∀X1,X0.[M->exert(order_condorcet_engine,s(exert(aggregate_utility_sum_engine,s(exert(assess_engine,ius),X0)),X1))]|∀X1,X0.[M->exert(order_condorcet_engine,s(exert(aggregate_utility_signed_engine,s(exert(assess_engine,ius),X0)),X1))]|∀X1,X0.[M->exert(order_condorcet_engine,s(exert(aggregate_utility_boolean_engine,s(exert(assess_engine,ius),X0)),X1))]|∀X1,X0.[M->exert(order_dominating_engine,s(exert(aggregate_utility_sum_engine,s(exert(assess_engine,ius),X0)),X1))]|∀X1,X0.[M->exert(order_lexicographical_engine,s(exert(aggregate_utility_sum_engine,s(exert(assess_engine,ius),X0)),X1))]|∀X1,X0.[M->exert(order_dominating_engine,s(exert(aggregate_utility_boolean_engine,s(exert(assess_engine,ius),X0)),X1))]|∀X1,X0.[M->exert(order_dominating_engine,s(exert(aggregate_utility_signed_engine,s(exert(assess_engine,ius),X0)),X1))]|∀X1,X0.[M->exert(order_lexicographical_engine,s(exert(aggregate_utility_boolean_engine,s(exert(assess_engine,ius),X0)),X1))]|∀X1,X0.[M->exert(order_lexicographical_engine,s(exert(aggregate_utility_signed_engine,s(exert(assess_engine,ius),X0)),X1))])|_] for test-decision-questions +% +% tff(question_decl, question, +% ?[M : modelet]: +% ( +% modelet_models_concept(M, weak_ordering) +% ) +% ). + + +%%% Test take +% +% Solved with this strategy: +% dis+1010_1:4_drc=ordering:aac=none:abs=on:atotf=0.5:avsq=on:avsqc=2:avsqr=215,247:bsd=on:erd=off:fde=none:gve=cautious:newcnf=on:nwc=5.0:rnwc=on:sac=on:sas=z3:sp=const_min:tgt=ground:thsq=on:thsqc=64:thsqr=1,4:i=59848:si=on:rawr=on:rtra=on_0 +% +% simplified to -s 1010 -sa discount -awr 1:4 +% +%%% Output +% SZS answers Tuple [(∀X6,X5,X4,X3,X2,X1,X0.[M->exert(take_best_engine,s(exert(order_condorcet_engine,s(exert(aggregate_utility_sum_engine,s(exert(assess_engine,s(X0,s(X1,s(X2,s(X3,ius))))),X4)),X5)),X6))]|∀X6,X5,X4,X3,X2,X1,X0.[M->exert(take_best_engine,s(exert(order_condorcet_engine,s(exert(aggregate_utility_signed_engine,s(exert(assess_engine,s(X0,s(X1,s(X2,s(X3,ius))))),X4)),X5)),X6))]|∀X6,X5,X4,X3,X2,X1,X0.[M->exert(take_best_engine,s(exert(order_condorcet_engine,s(exert(aggregate_utility_boolean_engine,s(exert(assess_engine,s(X0,s(X1,s(X2,s(X3,ius))))),X4)),X5)),X6))]|∀X5,X4,X3,X2,X1,X0.[M->exert(take_best_engine,s(exert(order_lexicographical_engine,s(exert(aggregate_utility_signed_engine,s(exert(assess_engine,s(X0,s(X1,s(X2,s(given_alternatives_modelet,ius))))),X3)),X4)),X5))]|∀X5,X4,X3,X2,X1,X0.[M->exert(take_best_engine,s(exert(order_dominating_engine,s(exert(aggregate_utility_signed_engine,s(exert(assess_engine,s(X0,s(X1,s(X2,s(given_alternatives_modelet,ius))))),X3)),X4)),X5))]|∀X5,X4,X3,X2,X1,X0.[M->exert(take_best_engine,s(exert(order_dominating_engine,s(exert(aggregate_utility_sum_engine,s(exert(assess_engine,s(X0,s(X1,s(X2,s(given_alternatives_modelet,ius))))),X3)),X4)),X5))]|∀X5,X4,X3,X2,X1,X0.[M->exert(take_best_engine,s(exert(order_lexicographical_engine,s(exert(aggregate_utility_sum_engine,s(exert(assess_engine,s(X0,s(X1,s(X2,s(given_alternatives_modelet,ius))))),X3)),X4)),X5))]|∀X5,X4,X3,X2,X1,X0.[M->exert(take_best_engine,s(exert(order_dominating_engine,s(exert(aggregate_utility_boolean_engine,s(exert(assess_engine,s(X0,s(X1,s(X2,s(given_alternatives_modelet,ius))))),X3)),X4)),X5))]|∀X5,X4,X3,X2,X1,X0.[M->exert(take_best_engine,s(exert(order_dominating_engine,s(exert(aggregate_preferences_engine,s(exert(assess_engine,s(X0,s(X1,s(X2,s(given_alternatives_modelet,ius))))),X3)),X4)),X5))]|∀X5,X4,X3,X2,X1,X0.[M->exert(take_best_engine,s(exert(order_lexicographical_engine,s(exert(aggregate_utility_boolean_engine,s(exert(assess_engine,s(X0,s(X1,s(X2,s(given_alternatives_modelet,ius))))),X3)),X4)),X5))]|∀X6,X5,X4,X3,X2,X1,X0.[M->exert(take_best_engine,s(exert(order_condorcet_engine,s(exert(aggregate_preferences_engine,s(exert(assess_engine,s(X0,s(X1,s(X2,s(X3,ius))))),X4)),X5)),X6))]|∀X5,X4,X3,X2,X1,X0.[M->exert(take_best_engine,s(exert(order_lexicographical_engine,s(exert(aggregate_preferences_engine,s(exert(assess_engine,s(X0,s(X1,s(X2,s(given_alternatives_modelet,ius))))),X3)),X4)),X5))]|∀X5,X4,X3,X2,X1,X0.[M->exert(eliminate_worst_engine,s(exert(order_lexicographical_engine,s(exert(aggregate_preferences_engine,s(exert(assess_engine,s(X0,s(X1,s(X2,s(given_alternatives_modelet,ius))))),X3)),X4)),X5))]|∀X5,X4,X3,X2,X1,X0.[M->exert(eliminate_worst_engine,s(exert(order_dominating_engine,s(exert(aggregate_preferences_engine,s(exert(assess_engine,s(X0,s(X1,s(X2,s(given_alternatives_modelet,ius))))),X3)),X4)),X5))]|∀X5,X4,X3,X2,X1,X0.[M->exert(eliminate_worst_engine,s(exert(order_dominating_engine,s(exert(aggregate_utility_sum_engine,s(exert(assess_engine,s(X0,s(X1,s(X2,s(given_alternatives_modelet,ius))))),X3)),X4)),X5))]|∀X5,X4,X3,X2,X1,X0.[M->exert(eliminate_worst_engine,s(exert(order_dominating_engine,s(exert(aggregate_utility_signed_engine,s(exert(assess_engine,s(X0,s(X1,s(X2,s(given_alternatives_modelet,ius))))),X3)),X4)),X5))]|∀X5,X4,X3,X2,X1,X0.[M->exert(eliminate_worst_engine,s(exert(order_dominating_engine,s(exert(aggregate_utility_boolean_engine,s(exert(assess_engine,s(X0,s(X1,s(X2,s(given_alternatives_modelet,ius))))),X3)),X4)),X5))]|∀X5,X4,X3,X2,X1,X0.[M->exert(eliminate_worst_engine,s(exert(order_lexicographical_engine,s(exert(aggregate_utility_sum_engine,s(exert(assess_engine,s(X0,s(X1,s(X2,s(given_alternatives_modelet,ius))))),X3)),X4)),X5))]|∀X2,X1,X0.[M->exert(eliminate_worst_engine,s(exert(order_lexicographical_engine,s(exert(aggregate_utility_signed_engine,s(exert(assess_engine,ius),X0)),X1)),X2))]|∀X5,X4,X3,X2,X1,X0.[M->exert(eliminate_worst_engine,s(exert(order_condorcet_engine,s(exert(aggregate_utility_sum_engine,s(exert(assess_engine,s(X0,s(X1,s(X2,s(given_alternatives_modelet,ius))))),X3)),X4)),X5))]|∀X5,X4,X3,X2,X1,X0.[M->exert(eliminate_worst_engine,s(exert(order_condorcet_engine,s(exert(aggregate_utility_boolean_engine,s(exert(assess_engine,s(X0,s(X1,s(X2,s(given_alternatives_modelet,ius))))),X3)),X4)),X5))]|∀X5,X4,X3,X2,X1,X0.[M->exert(eliminate_worst_engine,s(exert(order_condorcet_engine,s(exert(aggregate_utility_signed_engine,s(exert(assess_engine,s(X0,s(X1,s(X2,s(given_alternatives_modelet,ius))))),X3)),X4)),X5))]|∀X2,X1,X0.[M->exert(eliminate_worst_engine,s(exert(order_lexicographical_engine,s(exert(aggregate_utility_boolean_engine,s(exert(assess_engine,ius),X0)),X1)),X2))]|∀X5,X4,X3,X2,X1,X0.[M->exert(eliminate_worst_engine,s(exert(order_condorcet_engine,s(exert(aggregate_preferences_engine,s(exert(assess_engine,s(X0,s(X1,s(X2,s(given_alternatives_modelet,ius))))),X3)),X4)),X5))])|_] for test-decision-questions +% +% tff(question_decl, question, +% ?[M : modelet]: +% ( +% modelet_models_concept(M, alternative_array) +% & +% modelet_has_representation_class(M, choice) +% ) +% ). + + +%%% Test decision +% +% With just two accept engines, Solved with this strategy: +% dis+1010_1:4_drc=ordering:aac=none:abs=on:atotf=0.5:avsq=on:avsqc=2:avsqr=215,247:bsd=on:erd=off:fde=none:gve=cautious:newcnf=on:nwc=5.0:rnwc=on:sac=on:sas=z3:sp=const_min:tgt=ground:thsq=on:thsqc=64:thsqr=1,4:i=59848:si=on:rawr=on:rtra=on_0 on test-decision-questions for (300ds/59848Mi) +% +% simplified to: -s 1010 -sa discount -awr 1:4 -drc ordering -aac none -abs on -avsq on -avsqc 2 -avsqr 215,247 + +% lrs+1010_1:1_drc=ordering:aac=none:abs=on:bd=off:fd=off:nm=0:sas=z3:sims=off:tha=off:to=lpo:i=12098:si=on:rawr=on:rtra=on:si=on:rtra=on_0 +% Simplified to : -s 1010 -sa lrs -awr 1:1 -drc ordering -aac none -abs on -avsq on -avsqc 2 -avsqr 215,247 -bce on -bd off -fd off -nm 0 -sas z3 -sims off -tha off -to lpo -i 120980 -si on +% +% - removing z3 made a huge difference +% -s 1010 -sa lrs -awr 1:1 -drc ordering -aac none -abs on -avsq on -avsqc 2 -avsqr 215,247 -bce on -bd off -fd off -nm 0 -i 100000 -si on +% -s 1010 -amm off -aac none -abs on -avsq on -avsqc 2 -bd off -fd off -si on +% +% lrs+11_9:8_drc=ordering:amm=off:bsd=on:etr=on:fsd=on:fsr=off:lma=on:newcnf=on:nm=0:nwc=3.0:s2a=on:s2agt=10:sas=z3:tha=some:i=4725:si=on:rawr=on:rtra=on_0 +% lrs+1010_1:1_drc=ordering:bsr=unit_only:cond=on:flr=on:newcnf=on:nwc=10.0:sas=z3:to=lpo:i=360:si=on:rawr=on:rtra=on_0 +% +% lrs+1010_1:1_drc=ordering:bsr=unit_only:cond=on:flr=on:newcnf=on:nwc=10.0:sas=z3:to=lpo:i=360:si=on:rawr=on:rtra=on_0 +% Simplified to : -sa discount -s 1010 -nwc 10.0 + + + +%%% Output +% With only one accept engine: +% SZS answers Tuple [(∀X4,X3,X2,X1,X0.[M->exert(accept_always_engine,s(exert(eliminate_worst_engine,s(exert(order_dominating_engine,s(exert(aggregate_utility_signed_engine,s(exert(assess_engine,s(given_cues_modelet,s(given_alternatives_modelet,X0))),X1)),X2)),X3)),X4))]|∀X4,X3,X2,X1,X0.[M->exert(accept_always_engine,s(exert(eliminate_worst_engine,s(exert(order_dominating_engine,s(exert(aggregate_utility_boolean_engine,s(exert(assess_engine,s(given_cues_modelet,s(given_alternatives_modelet,X0))),X1)),X2)),X3)),X4))]|∀X4,X3,X2,X1,X0.[M->exert(accept_always_engine,s(exert(eliminate_worst_engine,s(exert(order_dominating_engine,s(exert(aggregate_preferences_engine,s(exert(assess_engine,s(given_cues_modelet,s(given_alternatives_modelet,X0))),X1)),X2)),X3)),X4))]|∀X4,X3,X2,X1,X0.[M->exert(accept_always_engine,s(exert(eliminate_worst_engine,s(exert(order_dominating_engine,s(exert(aggregate_utility_sum_engine,s(exert(assess_engine,s(given_cues_modelet,s(given_alternatives_modelet,X0))),X1)),X2)),X3)),X4))]|∀X4,X3,X2,X1,X0.[M->exert(accept_always_engine,s(exert(eliminate_worst_engine,s(exert(order_condorcet_engine,s(exert(aggregate_utility_signed_engine,s(exert(assess_engine,s(given_alternatives_modelet,s(given_cues_modelet,X0))),X1)),X2)),X3)),X4))]|∀X4,X3,X2,X1,X0.[M->exert(accept_always_engine,s(exert(eliminate_worst_engine,s(exert(order_lexicographical_engine,s(exert(aggregate_utility_signed_engine,s(exert(assess_engine,s(given_alternatives_modelet,s(given_cues_modelet,X0))),X1)),X2)),X3)),X4))]|∀X4,X3,X2,X1,X0.[M->exert(accept_always_engine,s(exert(eliminate_worst_engine,s(exert(order_condorcet_engine,s(exert(aggregate_preferences_engine,s(exert(assess_engine,s(given_alternatives_modelet,s(given_cues_modelet,X0))),X1)),X2)),X3)),X4))]|∀X4,X3,X2,X1,X0.[M->exert(accept_always_engine,s(exert(take_best_engine,s(exert(order_condorcet_engine,s(exert(aggregate_utility_sum_engine,s(exert(assess_engine,s(given_alternatives_modelet,s(given_cues_modelet,X0))),X1)),X2)),X3)),X4))]|∀X4,X3,X2,X1,X0.[M->exert(accept_always_engine,s(exert(take_best_engine,s(exert(order_condorcet_engine,s(exert(aggregate_utility_boolean_engine,s(exert(assess_engine,s(given_alternatives_modelet,s(given_cues_modelet,X0))),X1)),X2)),X3)),X4))]|∀X4,X3,X2,X1,X0.[M->exert(accept_always_engine,s(exert(eliminate_worst_engine,s(exert(order_lexicographical_engine,s(exert(aggregate_preferences_engine,s(exert(assess_engine,s(given_alternatives_modelet,s(given_cues_modelet,X0))),X1)),X2)),X3)),X4))]|∀X4,X3,X2,X1,X0.[M->exert(accept_always_engine,s(exert(take_best_engine,s(exert(order_lexicographical_engine,s(exert(aggregate_utility_boolean_engine,s(exert(assess_engine,s(given_alternatives_modelet,s(given_cues_modelet,X0))),X1)),X2)),X3)),X4))]|∀X4,X3,X2,X1,X0.[M->exert(accept_always_engine,s(exert(take_best_engine,s(exert(order_lexicographical_engine,s(exert(aggregate_utility_sum_engine,s(exert(assess_engine,s(given_alternatives_modelet,s(given_cues_modelet,X0))),X1)),X2)),X3)),X4))])|_] for test-decision-questions +% +% With only two accept engines: +% SZS answers Tuple [(∀X7,X6,X5,X4,X3,X2,X1,X0.[M->exert(accept_always_engine,s(exert(eliminate_worst_engine,s(exert(order_dominating_engine,s(exert(aggregate_utility_sum_engine,s(exert(assess_engine,s(X0,s(X1,s(X2,s(given_cues_modelet,s(given_alternatives_modelet,s(given_cues_modelet,X3))))))),X4)),X5)),X6)),X7))]|∀X8,X7,X6,X5,X4,X3,X2,X1,X0.[M->exert(accept_always_engine,s(exert(eliminate_worst_engine,s(exert(order_dominating_engine,s(exert(aggregate_preferences_engine,s(exert(assess_engine,s(X0,s(X1,s(X2,s(X3,s(X4,ius)))))),X5)),X6)),X7)),X8))]|∀X8,X7,X6,X5,X4,X3,X2,X1,X0.[M->exert(accept_always_engine,s(exert(eliminate_worst_engine,s(exert(order_dominating_engine,s(exert(aggregate_utility_boolean_engine,s(exert(assess_engine,s(X0,s(X1,s(X2,s(X3,s(X4,ius)))))),X5)),X6)),X7)),X8))]|∀X7,X6,X5,X4,X3,X2,X1,X0.[M->exert(accept_always_engine,s(exert(eliminate_worst_engine,s(exert(order_dominating_engine,s(exert(aggregate_utility_signed_engine,s(exert(assess_engine,s(X0,s(X1,s(X2,s(given_cues_modelet,s(given_alternatives_modelet,s(given_cues_modelet,X3))))))),X4)),X5)),X6)),X7))]|∀X8,X7,X6,X5,X4,X3,X2,X1,X0.[M->exert(accept_always_engine,s(exert(eliminate_worst_engine,s(exert(order_condorcet_engine,s(exert(aggregate_utility_sum_engine,s(exert(assess_engine,s(X0,s(X1,s(X2,s(X3,s(X4,ius)))))),X5)),X6)),X7)),X8))]|∀X8,X7,X6,X5,X4,X3,X2,X1,X0.[M->exert(accept_always_engine,s(exert(eliminate_worst_engine,s(exert(order_lexicographical_engine,s(exert(aggregate_utility_sum_engine,s(exert(assess_engine,s(X0,s(X1,s(X2,s(X3,s(X4,ius)))))),X5)),X6)),X7)),X8))]|∀X8,X7,X6,X5,X4,X3,X2,X1,X0.[M->exert(accept_always_engine,s(exert(eliminate_worst_engine,s(exert(order_condorcet_engine,s(exert(aggregate_utility_signed_engine,s(exert(assess_engine,s(X0,s(X1,s(X2,s(X3,s(X4,ius)))))),X5)),X6)),X7)),X8))]|∀X8,X7,X6,X5,X4,X3,X2,X1,X0.[M->exert(accept_always_engine,s(exert(eliminate_worst_engine,s(exert(order_condorcet_engine,s(exert(aggregate_utility_boolean_engine,s(exert(assess_engine,s(X0,s(X1,s(X2,s(X3,s(X4,ius)))))),X5)),X6)),X7)),X8))]|∀X8,X7,X6,X5,X4,X3,X2,X1,X0.[M->exert(accept_always_engine,s(exert(eliminate_worst_engine,s(exert(order_condorcet_engine,s(exert(aggregate_preferences_engine,s(exert(assess_engine,s(X0,s(X1,s(X2,s(X3,s(X4,ius)))))),X5)),X6)),X7)),X8))]|∀X8,X7,X6,X5,X4,X3,X2,X1,X0.[M->exert(accept_always_engine,s(exert(eliminate_worst_engine,s(exert(order_lexicographical_engine,s(exert(aggregate_utility_signed_engine,s(exert(assess_engine,s(X0,s(X1,s(X2,s(X3,s(X4,ius)))))),X5)),X6)),X7)),X8))]|∀X8,X7,X6,X5,X4,X3,X2,X1,X0.[M->exert(accept_always_engine,s(exert(eliminate_worst_engine,s(exert(order_lexicographical_engine,s(exert(aggregate_preferences_engine,s(exert(assess_engine,s(X0,s(X1,s(X2,s(X3,s(X4,ius)))))),X5)),X6)),X7)),X8))]|∀X8,X7,X6,X5,X4,X3,X2,X1,X0.[M->exert(accept_always_engine,s(exert(eliminate_worst_engine,s(exert(order_lexicographical_engine,s(exert(aggregate_utility_boolean_engine,s(exert(assess_engine,s(X0,s(X1,s(X2,s(X3,s(X4,ius)))))),X5)),X6)),X7)),X8))])|_] for test-decision-questions +% +% Without "hints" +% SZS answers Tuple [(∀X4,X3,X2,X1,X0.[M->exert(accept_dominating_engine,s(exert(eliminate_worst_engine,s(exert(order_condorcet_engine,s(exert(aggregate_preferences_engine,s(exert(assess_engine,s(given_alternatives_modelet,s(given_cues_modelet,X0))),X1)),X2)),X3)),X4))]|∀X4,X3,X2,X1,X0.[M->exert(accept_always_engine,s(exert(eliminate_worst_engine,s(exert(order_condorcet_engine,s(exert(aggregate_utility_sum_engine,s(exert(assess_engine,s(given_cues_modelet,s(given_alternatives_modelet,X0))),X1)),X2)),X3)),X4))]|∀X4,X3,X2,X1,X0.[M->exert(accept_always_engine,s(exert(eliminate_worst_engine,s(exert(order_condorcet_engine,s(exert(aggregate_utility_boolean_engine,s(exert(assess_engine,s(given_alternatives_modelet,s(given_cues_modelet,X0))),X1)),X2)),X3)),X4))]|∀X4,X3,X2,X1,X0.[M->exert(accept_always_engine,s(exert(eliminate_worst_engine,s(exert(order_condorcet_engine,s(exert(aggregate_utility_signed_engine,s(exert(assess_engine,s(given_alternatives_modelet,s(given_cues_modelet,X0))),X1)),X2)),X3)),X4))]|∀X4,X3,X2,X1,X0.[M->exert(accept_dominating_engine,s(exert(eliminate_worst_engine,s(exert(order_lexicographical_engine,s(exert(aggregate_utility_sum_engine,s(exert(assess_engine,s(given_cues_modelet,s(given_alternatives_modelet,X0))),X1)),X2)),X3)),X4))]|∀X4,X3,X2,X1,X0.[M->exert(accept_always_engine,s(exert(eliminate_worst_engine,s(exert(order_dominating_engine,s(exert(aggregate_utility_sum_engine,s(exert(assess_engine,s(given_alternatives_modelet,s(given_cues_modelet,X0))),X1)),X2)),X3)),X4))]|∀X4,X3,X2,X1,X0.[M->exert(accept_dominating_engine,s(exert(eliminate_worst_engine,s(exert(order_lexicographical_engine,s(exert(aggregate_utility_signed_engine,s(exert(assess_engine,s(given_alternatives_modelet,s(given_cues_modelet,X0))),X1)),X2)),X3)),X4))]|∀X4,X3,X2,X1,X0.[M->exert(accept_dominating_engine,s(exert(eliminate_worst_engine,s(exert(order_lexicographical_engine,s(exert(aggregate_preferences_engine,s(exert(assess_engine,s(given_alternatives_modelet,s(given_cues_modelet,X0))),X1)),X2)),X3)),X4))]|∀X4,X3,X2,X1,X0.[M->exert(accept_dominating_engine,s(exert(eliminate_worst_engine,s(exert(order_lexicographical_engine,s(exert(aggregate_utility_boolean_engine,s(exert(assess_engine,s(given_alternatives_modelet,s(given_cues_modelet,X0))),X1)),X2)),X3)),X4))]|∀X4,X3,X2,X1,X0.[M->exert(accept_always_engine,s(exert(eliminate_worst_engine,s(exert(order_dominating_engine,s(exert(aggregate_utility_signed_engine,s(exert(assess_engine,s(given_alternatives_modelet,s(given_cues_modelet,X0))),X1)),X2)),X3)),X4))]|∀X4,X3,X2,X1,X0.[M->exert(accept_dominating_engine,s(exert(eliminate_worst_engine,s(exert(order_dominating_engine,s(exert(aggregate_utility_boolean_engine,s(exert(assess_engine,s(given_alternatives_modelet,s(given_cues_modelet,X0))),X1)),X2)),X3)),X4))]|∀X4,X3,X2,X1,X0.[M->exert(accept_dominating_engine,s(exert(eliminate_worst_engine,s(exert(order_dominating_engine,s(exert(aggregate_preferences_engine,s(exert(assess_engine,s(given_alternatives_modelet,s(given_cues_modelet,X0))),X1)),X2)),X3)),X4))])|_] for test-decision-questions +% +% With only three accept engines: +% SZS answers Tuple [(∀X3,X2,X1,X0.[M->exert(accept_always_engine,s(exert(eliminate_worst_engine,s(exert(order_dominating_engine,s(exert(aggregate_utility_signed_engine,s(exert(assess_engine,ius),X0)),X1)),X2)),X3))]|∀X3,X2,X1,X0.[M->exert(accept_satisficing_engine,s(exert(eliminate_worst_engine,s(exert(order_dominating_engine,s(exert(aggregate_utility_boolean_engine,s(exert(assess_engine,ius),X0)),X1)),X2)),X3))]|∀X3,X2,X1,X0.[M->exert(accept_satisficing_engine,s(exert(eliminate_worst_engine,s(exert(order_dominating_engine,s(exert(aggregate_preferences_engine,s(exert(assess_engine,ius),X0)),X1)),X2)),X3))]|∀X4,X3,X2,X1,X0.[M->exert(accept_satisficing_engine,s(exert(eliminate_worst_engine,s(exert(order_dominating_engine,s(exert(aggregate_utility_sum_engine,s(exert(assess_engine,s(X0,ius)),X1)),X2)),X3)),X4))]|∀X4,X3,X2,X1,X0.[M->exert(accept_always_engine,s(exert(eliminate_worst_engine,s(exert(order_condorcet_engine,s(exert(aggregate_utility_signed_engine,s(exert(assess_engine,s(X0,ius)),X1)),X2)),X3)),X4))]|∀X4,X3,X2,X1,X0.[M->exert(accept_always_engine,s(exert(eliminate_worst_engine,s(exert(order_lexicographical_engine,s(exert(aggregate_utility_signed_engine,s(exert(assess_engine,s(X0,ius)),X1)),X2)),X3)),X4))]|∀X4,X3,X2,X1,X0.[M->exert(accept_dominating_engine,s(exert(take_best_engine,s(exert(order_lexicographical_engine,s(exert(aggregate_preferences_engine,s(exert(assess_engine,s(X0,ius)),X1)),X2)),X3)),X4))]|∀X4,X3,X2,X1,X0.[M->exert(accept_dominating_engine,s(exert(take_best_engine,s(exert(order_lexicographical_engine,s(exert(aggregate_utility_sum_engine,s(exert(assess_engine,s(X0,ius)),X1)),X2)),X3)),X4))]|∀X4,X3,X2,X1,X0.[M->exert(accept_dominating_engine,s(exert(take_best_engine,s(exert(order_lexicographical_engine,s(exert(aggregate_utility_boolean_engine,s(exert(assess_engine,s(X0,ius)),X1)),X2)),X3)),X4))]|∀X5,X4,X3,X2,X1,X0.[M->exert(accept_always_engine,s(exert(eliminate_worst_engine,s(exert(order_condorcet_engine,s(exert(aggregate_preferences_engine,s(exert(assess_engine,s(X0,s(X1,ius))),X2)),X3)),X4)),X5))]|∀X5,X4,X3,X2,X1,X0.[M->exert(accept_satisficing_engine,s(exert(take_best_engine,s(exert(order_condorcet_engine,s(exert(aggregate_utility_sum_engine,s(exert(assess_engine,s(X0,s(X1,ius))),X2)),X3)),X4)),X5))]|∀X5,X4,X3,X2,X1,X0.[M->exert(accept_satisficing_engine,s(exert(take_best_engine,s(exert(order_condorcet_engine,s(exert(aggregate_utility_boolean_engine,s(exert(assess_engine,s(X0,s(X1,ius))),X2)),X3)),X4)),X5))])|_] for test-decision-questions +% +% With all: +% SZS answers Tuple [(∀X3,X2,X1,X0.[M->exert(accept_size_engine,s(exert(eliminate_worst_engine,s(exert(order_condorcet_engine,s(exert(aggregate_utility_boolean_engine,s(exert(assess_engine,ius),X0)),X1)),X2)),X3))]|∀X3,X2,X1,X0.[M->exert(accept_always_engine,s(exert(eliminate_worst_engine,s(exert(order_dominating_engine,s(exert(aggregate_utility_boolean_engine,s(exert(assess_engine,ius),X0)),X1)),X2)),X3))]|∀X3,X2,X1,X0.[M->exert(accept_size_engine,s(exert(eliminate_worst_engine,s(exert(order_dominating_engine,s(exert(aggregate_utility_signed_engine,s(exert(assess_engine,ius),X0)),X1)),X2)),X3))]|∀X3,X2,X1,X0.[M->exert(accept_size_engine,s(exert(eliminate_worst_engine,s(exert(order_dominating_engine,s(exert(aggregate_utility_sum_engine,s(exert(assess_engine,ius),X0)),X1)),X2)),X3))]|∀X3,X2,X1,X0.[M->exert(accept_size_engine,s(exert(eliminate_worst_engine,s(exert(order_dominating_engine,s(exert(aggregate_preferences_engine,s(exert(assess_engine,ius),X0)),X1)),X2)),X3))]|∀X3,X2,X1,X0.[M->exert(accept_size_engine,s(exert(eliminate_worst_engine,s(exert(order_lexicographical_engine,s(exert(aggregate_preferences_engine,s(exert(assess_engine,ius),X0)),X1)),X2)),X3))]|∀X3,X2,X1,X0.[M->exert(accept_always_engine,s(exert(eliminate_worst_engine,s(exert(order_condorcet_engine,s(exert(aggregate_preferences_engine,s(exert(assess_engine,ius),X0)),X1)),X2)),X3))]|∀X3,X2,X1,X0.[M->exert(accept_size_engine,s(exert(eliminate_worst_engine,s(exert(order_condorcet_engine,s(exert(aggregate_utility_sum_engine,s(exert(assess_engine,ius),X0)),X1)),X2)),X3))]|∀X3,X2,X1,X0.[M->exert(accept_always_engine,s(exert(eliminate_worst_engine,s(exert(order_lexicographical_engine,s(exert(aggregate_utility_sum_engine,s(exert(assess_engine,ius),X0)),X1)),X2)),X3))]|∀X3,X2,X1,X0.[M->exert(accept_size_engine,s(exert(eliminate_worst_engine,s(exert(order_lexicographical_engine,s(exert(aggregate_utility_boolean_engine,s(exert(assess_engine,ius),X0)),X1)),X2)),X3))]|∀X3,X2,X1,X0.[M->exert(accept_size_engine,s(exert(eliminate_worst_engine,s(exert(order_lexicographical_engine,s(exert(aggregate_utility_signed_engine,s(exert(assess_engine,ius),X0)),X1)),X2)),X3))]|∀X3,X2,X1,X0.[M->exert(accept_always_engine,s(exert(eliminate_worst_engine,s(exert(order_condorcet_engine,s(exert(aggregate_utility_signed_engine,s(exert(assess_engine,ius),X0)),X1)),X2)),X3))])|_] for test-decision-questions +% +% + + +tff(question_decl, question, + ?[M : modelet]: + ( + modelet_models_concept(M, decision) + & + modelet_has_property(M, absolute_size_prop) + ) +). diff --git a/tff/tests/test-validate-structure-properties.tff b/tff/tests/test-validate-structure-properties.tff new file mode 100644 index 0000000..7e68f68 --- /dev/null +++ b/tff/tests/test-validate-structure-properties.tff @@ -0,0 +1,156 @@ +% Test Decision engines +include('understanding-logic/tff/domains/decision-system/engines.tff'). +%include('decision-logic/tff/model/decision-properties-fixed.tff'). + +%%% Decent strategy = lrs+1110_1:1_drc=ordering:bsd=on:fsr=off:nwc=3.0:s2a=on:s2agt=10:urr=on_0 + + +%%%%%% Requirements +%--------------------------------------------------------------------------- +%%% Absolute Size Requirement +%----------------------------------- +% tff(absolute_size_req_decl, type, +% absolute_size_req : requirement +% ). +% +% tff(absolute_size_req_datatype, axiom, +% datatype_of_requirement(absolute_size_req) = choice_size_datatype +% ). +% +% tff(abslute_size_permissible_value, axiom, +% ![N: $real]: +% ( +% is_permissible(absolute_size_req, N) +% <=> +% N = 1.0 +% ) +% ). +% %----------------------------------- +% %--------------------------------------------------------------------------- +% +% +% +% %%%%%% Templates +% %--------------------------------------------------------------------------- +% %%% Absolute Size Template +% %----------------------------------- +% tff(absolute_size_template_decl, type, +% absolute_size_template : template +% ). +% +% tff(absolute_size_template_requirements, axiom, +% ![R : requirement]: +% ( +% is_part_of(R, absolute_size_template) +% <=> +% R = absolute_size_req +% ) +% ). +% +% % tff(absolute_size_template_requirements, axiom, +% % ~?[R : requirement]: +% % is_part_of(R, absolute_size_template) +% % ). +% +% tff(absolute_size_template_no_creator_requirements, axiom, +% ~?[E: engine]: +% template_has_creator_requirement(absolute_size_template, E) +% ). +% +% tff(absolute_size_template_concept, axiom, +% ![C : concept]: +% ( +% template_has_concept_requirement(absolute_size_template, C) +% <=> +% C = decision +% ) +% ). +% +% tff(absolute_size_template_formalism, axiom, +% template_formalism_requirement(absolute_size_template) = decision_msg +% ). +% +% tff(absolute_size_template_no_representation_class, axiom, +% ~?[R : representation_class]: +% template_has_representation_class_requirement(absolute_size_template, R) +% ). +% +% tff(absolute_size_template_no_location_requirements, axiom, +% ~?[SPT: spacetime_point]: +% template_has_location_requirement(absolute_size_template, SPT) +% ). +% +% tff(absolute_size_template_no_extent_requirements, axiom, +% ~?[E: extent]: +% template_has_extent_requirement(absolute_size_template, E) +% ). +% %----------------------------------- +% +% tff(template_distinct_from_others, axiom, +% ( +% absolute_size_template != cue_array_template +% & +% absolute_size_template != assessment_matrix_template +% & +% absolute_size_template != evaluation_template +% & +% absolute_size_template != weak_ordering_template +% & +% absolute_size_template != choice_template +% ) +% ). +% +% %--------------------------------------------------------------------------- +% +% +% +% %%%%%% Questions +% %--------------------------------------------------------------------------- +% +% tff(set_param_value, axiom, +% has_value(absolute_size_prop) = 1.0 +% ). + +% Is there a modelet that matches the absolute_size template +% tff(question_decl, question, +% ?[M : modelet] : +% ( +% inputs_match(M, absolute_size_template) +% ) +% ). +tff(no_engine_requirements, axiom, + ![R: requirement]: + ~is_active(R) +). + +tff(question_decl, conjecture, + ?[M : modelet, MS0a : modelet_set, MS0b : modelet_set, MS1 : modelet_set, MS2 : modelet_set, MS3 : modelet_set, MS4 : modelet_set]: + ( + ( + s(exert(update_alternatives_elim_engine, empty_ms), empty_ms) = MS0a + & + s(exert(update_cues_take_the_best_engine, MS0a), MS0a) = MS0b + & + s(exert(assess_engine, MS0b), MS0b) = MS1 + & + s(exert(aggregate_preferences_engine, MS1), MS1) = MS2 + & + s(exert(order_lexicographical_engine, MS2), MS2) = MS3 + & + s(exert(eliminate_worst_engine, MS3), MS3) = MS4 + & + exert(accept_size_engine, MS4) = M + ) + % & + % inputs_match(M, absolute_size_template) + => + ( + modelet_models_concept(M, decision) + & + modelet_has_property(M, absolute_size_prop) + ) + ) +). + + +%--------------------------------------------------------------------------- diff --git a/tff/tests/test-wind-scenario.tff b/tff/tests/test-wind-scenario.tff index 7a071ed..82d6ce7 100644 --- a/tff/tests/test-wind-scenario.tff +++ b/tff/tests/test-wind-scenario.tff @@ -490,9 +490,9 @@ tff(dse_engine_output_representation_class, axiom, is_output_modelet_representation_class(dse_engine, R) ). - tff(dse_engine_defined_input, axiom, +tff(dse_engine_defined_input, axiom, defines_input2(gnss_template, imu_template, dse_engine) - ). +). @@ -555,6 +555,11 @@ tff(wee_engine_defined_input, axiom, ). +tff(no_engine_requirements, axiom, + ![R: requirement]: + ~is_active(R) +). + tff(question_decl, question, ?[M : modelet]: