package verificationClasses;

import splkorat.ElevatorSpecOneKORAT;

public class FeatureSwitches {
/*
 * DO NOT EDIT! THIS FILE IS AUTOGENERATED BY fstcomp 
 */

//public static boolean __SELECTED_FEATURE_base;
public static boolean __SELECTED_FEATURE_weight;
public static boolean __SELECTED_FEATURE_empty;
public static boolean __SELECTED_FEATURE_twothirdsfull;
public static boolean __SELECTED_FEATURE_executivefloor;
public static boolean __SELECTED_FEATURE_overloaded;

public static String getSelectedFeaturesAsNames() {
StringBuilder sb = new StringBuilder();
	if (__SELECTED_FEATURE_weight) sb.append("weight;");
	if (__SELECTED_FEATURE_twothirdsfull) sb.append("twothirdsfull;");
	if (__SELECTED_FEATURE_empty) sb.append("empty;");
	if (ElevatorSpecOneKORAT.get_BASE___()) sb.append("base;");
	if (__SELECTED_FEATURE_overloaded) sb.append("overloaded;");
	if (__SELECTED_FEATURE_executivefloor) sb.append("executivefloor;");
return sb.toString();
}

/*
public static void select_features() {
	__SELECTED_FEATURE_weight = verificationClasses.SPLModelChecker.getBoolean();
	__SELECTED_FEATURE_twothirdsfull = verificationClasses.SPLModelChecker.getBoolean();
	__SELECTED_FEATURE_empty = verificationClasses.SPLModelChecker.getBoolean();
	__SELECTED_FEATURE_base = verificationClasses.SPLModelChecker.getBoolean();
	__SELECTED_FEATURE_overloaded = verificationClasses.SPLModelChecker.getBoolean();
	__SELECTED_FEATURE_executivefloor = verificationClasses.SPLModelChecker.getBoolean();
} */

public static boolean __GUIDSL_ROOT_PRODUCTION;

public static void select_helpers() {
	__GUIDSL_ROOT_PRODUCTION = true;
}

public static boolean valid_product() {
	if ((( !__SELECTED_FEATURE_overloaded || __SELECTED_FEATURE_weight ) && ( !__SELECTED_FEATURE_twothirdsfull || __SELECTED_FEATURE_weight )) && ( __SELECTED_FEATURE_base ))
		return true;
	else
		return false;
}
}